{"push_id":1681469617,"size":23,"distinct_size":1,"ref":"refs/heads/remove-vernacerror","head":"9dc88fb4b5ea6d1de1b817c65d17b0c95eda6443","before":"e7e2c7fed265d6d421634449f14f0fa1336474ac","commits":[{"sha":"fedc831df9626a31cd0d26ee6b9e022b67f90c2a","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing a little bug in using the \"where\" clause for inductive types.\n\nThis was not working when the inductive type had implicit parameters.\n\nThis could still be improved. E.g. the following still does not work:\n\nReserved Notation \"#\".\nInductive I {A:Type} := C : # where \"#\" := I.\n\nBut it should be made working by taking care of adding the mandatory\nimplicit argument A at the time # is interpreted as [@I _]\n(i.e., technically speaking, using expl_impls in interp_notation).","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/fedc831df9626a31cd0d26ee6b9e022b67f90c2a"},{"sha":"8451b4ae99b448894a6269c08be7f3ac0d74cac4","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing a little bug in printing ex2 (type was printed \"_\" by default).","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/8451b4ae99b448894a6269c08be7f3ac0d74cac4"},{"sha":"ed25677029e2cc1e34eba76aade1a00980ca11de","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing anomaly on unsupported key in interactive ltac debug.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/ed25677029e2cc1e34eba76aade1a00980ca11de"},{"sha":"209ff6ae4367b8c96b59bc318f4791dcb2251c14","author":{"name":"Tej Chajed","email":"407dbab6d446ed7a7635912097af2063578b5c29@mit.edu"},"message":"Correctly identify [Time Defined.] as a defined\n\nNeed to check inside control expressions. Also fixes handling of\n[Redirect \"file\" Defined.] and [Timeout n Defined.].\n\nFixes Coq bug 5411 (https://coq.inria.fr/bugs/show_bug.cgi?id=5411):\ncoqc -quick hangs on [Time Defined.]","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/209ff6ae4367b8c96b59bc318f4791dcb2251c14"},{"sha":"ca0d97dd3b3033e7f87dd5e5ea09ab6f14fd881b","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Fix bug #5435: [Eval native_compute in] raises anomaly.\n\nWas introduced by 4f041384cb27f0d2. Unsoundness seems miraculously\navoided by a safeguard I put in nativecode.ml. But other kernel changes\nin this commit should probably be reviewed carefully.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/ca0d97dd3b3033e7f87dd5e5ea09ab6f14fd881b"},{"sha":"70bcfcf5b2ea485ebe253158c37b89dfac63820b","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Test file for #5435:  [Eval native_compute in] raises anomaly.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/70bcfcf5b2ea485ebe253158c37b89dfac63820b"},{"sha":"57c673d0aa411facc2fc8fa222e7653041b282ea","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR#535: Fix #5435: [Eval native_compute in] raises anomaly.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/57c673d0aa411facc2fc8fa222e7653041b282ea"},{"sha":"c6f24b1cbfb485dbf14b3934208c113140de2eca","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing #5454 (an assert false with 'pat).\n\nNote: Apparently not easy to make a test file as the error is raised\nin \"G_vernac.fresh_var\" at parsing time (not captured by Fail).","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/c6f24b1cbfb485dbf14b3934208c113140de2eca"},{"sha":"33f40197e6b7bef02c8df2dc0a0066f8144b66d6","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Merge branch 'origin/v8.5' into v8.6.\n\nWas needed to be done for a while.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/33f40197e6b7bef02c8df2dc0a0066f8144b66d6"},{"sha":"48c44b55b76e75aa2af9f82753c6ffe7531790c8","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Fix a few programming pearls related to Time, Fail and Redirect.\n\nThis fixes a few clear bugs, but the STM code handling Time, Fail and\nRedirect before par: still needs to be rewritten. It does not implement\nthe same semantics as the vernac interpreter for Fail Fail [c] and\nignores Redirect.\n\nThis commit was already reviewed with Enrico and tested on Travis.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/48c44b55b76e75aa2af9f82753c6ffe7531790c8"},{"sha":"007ab31b4d1b9457d2758a614aed5a49dee53b62","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing #5460 (limitation in computing deps in pattern-matching compilation).\n\nThis was assuming dependencies occurring in configurations of\nthe form x:A, y:B x, z:C x y |- match x, y, z with ... end\".\n\nBut still work to do for better management of dependencies in general...","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/007ab31b4d1b9457d2758a614aed5a49dee53b62"},{"sha":"582fab072375924ce380148c8a92dbc2b4ec30cc","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR#510: Correctly identify [Time Defined.] as a defined","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/582fab072375924ce380148c8a92dbc2b4ec30cc"},{"sha":"865fa8fc7aacbca3ab167e65f56e280d334eb192","author":{"name":"Paul Steckler","email":"3e28969a28708413e246320f9a89f07a222cf45c@stecksoft.com"},"message":"add XML protocol doc for 8.5","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/865fa8fc7aacbca3ab167e65f56e280d334eb192"},{"sha":"6ef2dc11653e0572db6f7660470242ed23a0bdc2","author":{"name":"Paul Steckler","email":"3e28969a28708413e246320f9a89f07a222cf45c@stecksoft.com"},"message":"update XML protocol doc to 8.6","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/6ef2dc11653e0572db6f7660470242ed23a0bdc2"},{"sha":"ba1ff58db4aac8315e42acb598770d1aa67385ce","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"[travis] Use the lite target for fiat-crypto.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/ba1ff58db4aac8315e42acb598770d1aa67385ce"},{"sha":"273f8338f14473d4031fc2d1e5b80b5ad963adeb","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR#563: add XML protocol doc for 8.6","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/273f8338f14473d4031fc2d1e5b80b5ad963adeb"},{"sha":"e73b124a9d504e1759d4a4a0d3899882f58d459a","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"Fix anomaly when doing [all:Check _.] during a proof.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/e73b124a9d504e1759d4a4a0d3899882f58d459a"},{"sha":"1c0fcb97ac717c43a27f7e70702a548b07cfb041","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge PR#556: Fix anomaly when doing [all:Check _.] during a proof.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/1c0fcb97ac717c43a27f7e70702a548b07cfb041"},{"sha":"74f9548a083409d400f2723ee8c1e07705da4812","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Fix EOL characters in xml protocol documentation.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/74f9548a083409d400f2723ee8c1e07705da4812"},{"sha":"53a50875b28ad96ab1559ca3f97db5133ca5c78e","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing bug #5469 (notation format not recognizing curly braces).","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/53a50875b28ad96ab1559ca3f97db5133ca5c78e"}]}
{"actor":{"display_login":"SkySkimmer"}}