{"push_id":702956352,"size":644,"distinct_size":331,"ref":"refs/heads/trunk","head":"29fcfc4f8bc1bfbdfbae0c07850aed65f6c3eb04","before":"a0423c8c0051323ceb80f1786b75c54d3405b1ad","commits":[{"sha":"498d22e9575ecf2515ae592a07b3f50e7648882f","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it was\nactually calling the VM at Qed time.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/498d22e9575ecf2515ae592a07b3f50e7648882f"},{"sha":"bef0d3bc629e25a281b4ed2424dc3b8405349acf","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Making unification of LetIn's expressions more consistent (see #3920).\n\nUnifying two let-in's expresions syntactically is a heuristic\n(compared to performing the zeta-reduction). This heuristic was\nrequiring unification of types which is too strong for the heuristic\nto work uniformly since the types might only be related modulo\nsubtyping.\n\nThe patch is to remove the unification of types, which allows then to\nhave the heuristic work uniformly on the bodies. On the other side, I\nhope it does not loose (still heuristical) unifications compared to\nbefore (presumably, since instantiating the evars in the body will\ninduce constraints for solving potential evars in the types of the\nlet-in bodies, but this would need a proof). Anyway, it is not about\ncorrection, it is about a heuristic, which maybe done too early\nactually.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/bef0d3bc629e25a281b4ed2424dc3b8405349acf"},{"sha":"35fde66d67a7a4e36f04adc53347bbb87a34356e","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Fix a critical bug in machine arithmetic for native compiler.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/35fde66d67a7a4e36f04adc53347bbb87a34356e"},{"sha":"fb860f9ea8dca5395ca9f2f350a68c1760c84ce4","author":{"email":"1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","name":"Arnaud Spiwack"},"message":"Reference manual: fix typo in doc of [tryif/then/else].\n\nFixes #3939.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/fb860f9ea8dca5395ca9f2f350a68c1760c84ce4"},{"sha":"2e1ab34a9feaa3fac6220400acbc7c710b0a0211","author":{"email":"1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","name":"Arnaud Spiwack"},"message":"Reference manual: pass over the credit section for English.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/2e1ab34a9feaa3fac6220400acbc7c710b0a0211"},{"sha":"9e7e259e9f81eefd505b04e5e17b06136055e1ee","author":{"email":"1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","name":"Arnaud Spiwack"},"message":"Reference Manual/Credits: remove a duplicate.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/9e7e259e9f81eefd505b04e5e17b06136055e1ee"},{"sha":"5b653d2bb4d9f7b4c6f1faf4b3c17d6400cadf48","author":{"email":"1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","name":"Arnaud Spiwack"},"message":"Reference manual/Credits: populate the \"various smaller-scale improvements\" part.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/5b653d2bb4d9f7b4c6f1faf4b3c17d6400cadf48"},{"sha":"b855224b5ce5deda9853af1bed9b135a7ea9a76b","author":{"email":"1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","name":"Arnaud Spiwack"},"message":"Reference Manual/Credits: native compute is a major contribution.\n\nIt is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/b855224b5ce5deda9853af1bed9b135a7ea9a76b"},{"sha":"3527a32a9c055a1438f0c85b77d3dbd8d38cbd32","author":{"email":"1a340065606634b575ed162e9c434c27fe24a7c3@spiwack.net","name":"Arnaud Spiwack"},"message":"Reference Manual/Credits: expand the paragraph on the new proof engine to match the overall style.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/3527a32a9c055a1438f0c85b77d3dbd8d38cbd32"},{"sha":"feca7916eaaceea96be4c15f08895578b3703a1c","author":{"email":"367bbdfafbbc1a3248435237fe8f192500cc470e@gmail.com","name":"mlasson"},"message":"Add the possibility of defining opaque terms with program.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/feca7916eaaceea96be4c15f08895578b3703a1c"},{"sha":"4f632721be8b083126f49dd900a3294521879ec4","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Extraction: fix #3629.\n\nThe control flow of extraction is hard to read due to exceptions. When meeting\nan inlined constant extracted to custom code, they could desynchronize some\ntables in charge of detecting name clashes, leading to an anomaly.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/4f632721be8b083126f49dd900a3294521879ec4"},{"sha":"87106cd6a0e613fc61943959d8fc7d3ff025fc5d","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Merge branch 'v8.5' into trunk","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/87106cd6a0e613fc61943959d8fc7d3ff025fc5d"},{"sha":"09b5e429cd4f622003277c31391bafc20b389af5","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Typos, grammar, layout in CHANGES.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/09b5e429cd4f622003277c31391bafc20b389af5"},{"sha":"c930010fc53531784485d5a190f9c0aeba1dfdbe","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Typos, grammar, layout in CHANGES (continued).","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/c930010fc53531784485d5a190f9c0aeba1dfdbe"},{"sha":"a9026275399a891d47f0d10f624a783a1afea05d","author":{"email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr","name":"Maxime Dénès"},"message":"Fix previous commit on extraction.\n\nSince name clashes are discovered by side effects, the order of traversal of\nmodule structs cannot be changed.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/a9026275399a891d47f0d10f624a783a1afea05d"},{"sha":"43c6f29edde078726f10144c0d241a882ebdd13d","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Splitting ML tactics in one function per grammar entry.\n\nFurthermore, ML tactic dispatch is not done according to the\ntype of its argument anymore.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/43c6f29edde078726f10144c0d241a882ebdd13d"},{"sha":"f4d77142a6e1d298fadf4219c46fcc9ff8abe62a","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Tentative workaround for bug #3798.\n\nUltimately setoid rewrite should be written in the monad to fix it properly.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/f4d77142a6e1d298fadf4219c46fcc9ff8abe62a"},{"sha":"ef61bb05911d19c77d565d78dc57107d40c333e4","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Isolate a function for printing evar sets.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/ef61bb05911d19c77d565d78dc57107d40c333e4"},{"sha":"982b583efe9f657d76b4257200769fed55453623","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Equality Schemes options: reverting commit ff9f94634 which is\nobviously inconsistent with the decisions taken in commits\n2e8fb20e04da and 0bc569026048 about bugs #2550 and #3606.\n\nNow having options Boolean Equality Schemes and Decidable Equality Schemes.","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/982b583efe9f657d76b4257200769fed55453623"},{"sha":"14787df2ea09994151e886bf918aca0aecbd8ade","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Reference Manual: Documenting new printing of evars and new effect of\nSet Printing Existential Instances (see bug report #3951).","distinct":false,"url":"https://api.github.com/repos/mlasson/coq/commits/14787df2ea09994151e886bf918aca0aecbd8ade"}]}