{"push_id":1586764467,"size":367,"distinct_size":1,"ref":"refs/heads/v8.5-format-debug-NOPUSH-IN-OFFICIAL","head":"ff8264bc4901e7c7494bc80751c4f2efb12632b6","before":"8194f37a2e7d57b775bcfffd1f9d2c3fe09c30ba","commits":[{"sha":"5b4e3ace20eb2ab569d172a1f358f26f451d361c","author":{"name":"Jason Gross","email":"d3dfe5c5fac772d904d4932d138136d040bb63c7@mit.edu"},"message":"Move compatibility notations to their proper files","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/5b4e3ace20eb2ab569d172a1f358f26f451d361c"},{"sha":"f65f8d5a4d9ba437fa2d8af03e2781d841e53007","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Restore warnings produced by the interpretation of the command line\n(e.g. with deprecated options such as -byte, etc.) since I guess this\nis what we expect.\n\nWas probably lost in 81eb133d64ac81cb.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/f65f8d5a4d9ba437fa2d8af03e2781d841e53007"},{"sha":"ccdc62a6b4722c38f2b37cbf21b14e5094255390","author":{"name":"Matthieu Sozeau","email":"451d3b825623fdfe0dafc0e4827303e73a984a0e@inria.fr"},"message":"Fix bug #4506. Using betadeltaiota_nolet might produce terms of the form\n(let x := t in u) a that should be reduced. Maybe a different\ndecomposition/reduction primitive should be used instead.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/ccdc62a6b4722c38f2b37cbf21b14e5094255390"},{"sha":"5cbcc8fd761df0779f6202fef935f07cfef8a228","author":{"name":"Matthieu Sozeau","email":"451d3b825623fdfe0dafc0e4827303e73a984a0e@inria.fr"},"message":"Implement support for universe binder lists in Instance and Program Fixpoint/Definition.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/5cbcc8fd761df0779f6202fef935f07cfef8a228"},{"sha":"6a046f8d3e33701d70e2a391741e65564cc0554d","author":{"name":"Matthieu Sozeau","email":"451d3b825623fdfe0dafc0e4827303e73a984a0e@inria.fr"},"message":"Fix bug #4519: oops, global shadowed local universe level bindings.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/6a046f8d3e33701d70e2a391741e65564cc0554d"},{"sha":"b582db2ecbb3f7f1315fedc50b0009f62f5c59ad","author":{"name":"Matthieu Sozeau","email":"451d3b825623fdfe0dafc0e4827303e73a984a0e@inria.fr"},"message":"Fix bug #4503: mixing universe polymorphic and monomorphic\nvariables and definitions in sections is unsupported.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/b582db2ecbb3f7f1315fedc50b0009f62f5c59ad"},{"sha":"4b1103dc38754917e12bf04feca446e02cf55f07","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Fixing bug #4511: evar tactic can create non-typed evars.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/4b1103dc38754917e12bf04feca446e02cf55f07"},{"sha":"cb30837323aa462df24ad6668790f67b9bf20b5d","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Fixing bug #4495: Failed assertion in metasyntax.ml.\n\nWe simply handle the \"break\" in error messages. Not sure it is the\nproper bugfix though, we may want to be able to add breaks in such\nrecursive notations.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/cb30837323aa462df24ad6668790f67b9bf20b5d"},{"sha":"e7852396a452f446135183ec3e1743b731d781c0","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Adding a test for bug #4378.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/e7852396a452f446135183ec3e1743b731d781c0"},{"sha":"030ef2f015e5c592ea7599f0f98a715873c1e4d0","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Fixing bug #3826: \"Incompatible module types\" is uninformative.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/030ef2f015e5c592ea7599f0f98a715873c1e4d0"},{"sha":"f17096fa9eff103f40e6d381ebeb4313002fa378","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Fixing bug #4373: coqdep does not know about .vio files.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/f17096fa9eff103f40e6d381ebeb4313002fa378"},{"sha":"5361b02a96704a226b713b6040b67ca01de808fa","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Tentative fix for bug #4522: Incorrect \"Warning...\" on windows.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/5361b02a96704a226b713b6040b67ca01de808fa"},{"sha":"40cc1067dc5353d43ea2f6643cd8ca954e3e8afa","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing bde12b70 about reporting ill-formed constructor.\n\nFor instance, in\n\nInductive I : nat -> nat -> Prop := C : forall z, let '(x,y) := z in  x + y = 0.\n\nthe computation of the number of arguments to I was made wrong in bde12b70.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/40cc1067dc5353d43ea2f6643cd8ca954e3e8afa"},{"sha":"22a2cc1897f0d9f568ebfb807673e84f6ada491a","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Fix bug #4537: Coq 8.5 is slower in typeclass resolution.\n\nThe performance enhancement introduced by a895b2c0 for non-polymorphic hints\nwas actually causing a huge regression in the polymorphic case (and was marked\nas such). We fix this by only substituting the metas from the evarmap instead\nof the whole evarmap.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/22a2cc1897f0d9f568ebfb807673e84f6ada491a"},{"sha":"7eeec8f82d96a71929289b0b9401a1b96e1d3dda","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"More compact representation for evar resolvability flag.\n\nThis patch was proposed by JH in bug report #4547.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/7eeec8f82d96a71929289b0b9401a1b96e1d3dda"},{"sha":"0ee0b7d2f2365da6e63bc2e94d66f9c5fe1ebe6a","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Opacifying the type of evar naming structure in Evd.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/0ee0b7d2f2365da6e63bc2e94d66f9c5fe1ebe6a"},{"sha":"62c141be71dd3c542824c19429eac0fdd686c9cb","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimizing the computation of frozen evars.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/62c141be71dd3c542824c19429eac0fdd686c9cb"},{"sha":"5d9eaa378277ed96456fec5a2037a8da4f38c8e0","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimizing the universes_of_constr_function.\n\nInstead of relying on a costly set union, we take advantage of the fact\nthat instances are small compared to the set of universes.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/5d9eaa378277ed96456fec5a2037a8da4f38c8e0"},{"sha":"68db732f12980e592c610085192d93457f312607","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Improving error message with missing patterns in the presence of\nmultiple patterns.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/68db732f12980e592c610085192d93457f312607"},{"sha":"5f29a92c0648afd4d9e46de79ab00d0c4b901ff0","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"Don't fail fatally if PATH is not set.\n\nThis fixes micromega in certain environments.","distinct":false,"url":"https://api.github.com/repos/Matafou/coq/commits/5f29a92c0648afd4d9e46de79ab00d0c4b901ff0"}]}
{"actor":{"display_login":"Matafou"}}