{"push_id":1344753283,"size":146,"distinct_size":3,"ref":"refs/heads/trunk+a-few-iff-zarith-lemmas","head":"b463748abb03e633acc1a4220efb30b4a7eb940a","before":"36042b2935641369d72152a2a255a2db0e6b3685","commits":[{"sha":"fd47b2d2638518fe62ce9c63557d2dab219d9558","author":{"name":"Cyprien Mangin","email":"f8360d742f8012d00b6eea992cbcdaa81937a9d7@m4x.org"},"message":"Goal selectors now use the keyword [only].\n\nThis fixes some parsing problems when doing things like\n[let n := 2 in idtac n]. See bug #4877.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/fd47b2d2638518fe62ce9c63557d2dab219d9558"},{"sha":"4b61c0693d453dd0026792185354d68ba1db9022","author":{"name":"Cyprien Mangin","email":"f8360d742f8012d00b6eea992cbcdaa81937a9d7@m4x.org"},"message":"Update the documentation for goal selectors.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/4b61c0693d453dd0026792185354d68ba1db9022"},{"sha":"411973d14a95b043f93ed6d0ca628a6a98e3c221","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[checker] Fix/fine tune printing.\n\nIn 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct\naccess to the console, recommending instead to provide information to\nthe user by means of the `Feedback.msg_*` facilities.\n\nHowever, we introduced a display bug in the checker printer as it is\nspecial and doesn't use the Pp facilities (likely for trust reasons),\nspotted by @herbelin\n\nThis patch fixes this bug and performs a couple more of fine tunings in\nthe input.\n\nHowever, it could be desirable to port the `checker/printer.ml` to `Pp`\nand use the feedback mechanism; this would allow IDEs to use the checker\nin a more convenient way, at the cost of trusting `Pp` (which is already\na bit trusted currently)\n\nA start of that idea can be found at:\nhttps://github.com/ejgallego/coq/tree/fix_checker_printing","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/411973d14a95b043f93ed6d0ca628a6a98e3c221"},{"sha":"dfac5aa2285de5b89f08ada3c30c0a1594737440","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Making Vernacexpr independent from Tacexpr.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/dfac5aa2285de5b89f08ada3c30c0a1594737440"},{"sha":"ae9f6d13b63f30168d2eaa2289108a117ad840f7","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Unplugging Tacexpr in several interface files.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/ae9f6d13b63f30168d2eaa2289108a117ad840f7"},{"sha":"1654b3989041b25e3b642ffde12125344342a54b","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Making Hints generic in the use of external tactics.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/1654b3989041b25e3b642ffde12125344342a54b"},{"sha":"52c3917be7239f7d5ab1ba882275b4571463f585","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Making Proof_global terminator generic in external tactics.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/52c3917be7239f7d5ab1ba882275b4571463f585"},{"sha":"7045848145c16d978456aab2edd192c54d242e69","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Unplugging Pptactic from Ppvernac.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/7045848145c16d978456aab2edd192c54d242e69"},{"sha":"a6cd6948fa592f21b67916f423fe2adb62085492","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Removing the last uses of Pptactic in the lower layers.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/a6cd6948fa592f21b67916f423fe2adb62085492"},{"sha":"5466267afa78cac5479a503338fbc57d77f05458","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Move Ltac-specific components from G_proofs to G_ltac.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/5466267afa78cac5479a503338fbc57d77f05458"},{"sha":"5b1a15b5c561ed02335050f45ad123f8d548cee4","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Allowing to extend the Print Grammar command generically.\n\nWe also move the Ltac-specific grammar to its folder.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/5b1a15b5c561ed02335050f45ad123f8d548cee4"},{"sha":"16675c67c56456f6082c4da7c7657aaa2b1da375","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Moving the tactic-in-term extension from G_constr to G_ltac.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/16675c67c56456f6082c4da7c7657aaa2b1da375"},{"sha":"699b70cd9ad0d79cbde228bdb51fde224a3b524e","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Moving Ltac-specific parsing API to ltac/ folder.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/699b70cd9ad0d79cbde228bdb51fde224a3b524e"},{"sha":"404a8c619f76c572aec65f413baf087a374b37c3","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Generalizing the notion of constr substitution to generic arguments.\n\nThis removes a dependency on wit_tactic in Constrintern.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/404a8c619f76c572aec65f413baf087a374b37c3"},{"sha":"21dc493a93853525c5d9c33c0c7558909ce5e79d","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Moving Ltac printers to ltac/ folder.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/21dc493a93853525c5d9c33c0c7558909ce5e79d"},{"sha":"975e7cd2ad032668c7df690c9bdaa8cdbb196569","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Moving Ltac-specific generic arguments to their own file in the ltac/ folder.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/975e7cd2ad032668c7df690c9bdaa8cdbb196569"},{"sha":"1d432a8e7a2e728f0dbf909f95337f0ff2c33945","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Moving Tactic_matching to ltac/ folder.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/1d432a8e7a2e728f0dbf909f95337f0ff2c33945"},{"sha":"745c5325d79e754faecd0e1db75744f436f61a3b","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Typo.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/745c5325d79e754faecd0e1db75744f436f61a3b"},{"sha":"ccbb78b17fada5d9f0f5937dc276cb0b0960f4c3","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Continuing fix to #5078, taking also into account intropatterns.\nGetting closer from before when the bug was introduced + test.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/ccbb78b17fada5d9f0f5937dc276cb0b0960f4c3"},{"sha":"6eede071cb97e1e39772c2bdecb5189c4fa2adb0","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Extending \"contradiction\" so that it recognizes statements such as \"~x=x\" or ~True.\n\nFound 1 incompatibility in tested contribs and 3 times the same\npattern of incompatibility in the standard library. In all cases, it\nis an improvement in the form of the script.\n\nNew behavior deactivated when version is <= 8.5.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/6eede071cb97e1e39772c2bdecb5189c4fa2adb0"}]}
{"actor":{"display_login":"herbelin"}}