{"push_id":1177353005,"size":32,"distinct_size":27,"ref":"refs/heads/trunk","head":"403c12ac3e8a9c3719aacbfa113600abc74846b7","before":"861f385008d6c7f4a1a03f66589d34e974f0a341","commits":[{"sha":"9165bd2489842af64dbe098ed5906fe69e687bfe","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Better algorithm for variable deambiguation in term printing.\n\nWe do not recompute shortest name identifier for global references that were\nalready traversed. Furthermore, we share the computation of identifiers\nbetween invokations of the name generating function.\n\nThis drastically speeds up detyping for huge goals, further mitigating the\nshortcomings of the fix for bug #4777.","distinct":false,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/9165bd2489842af64dbe098ed5906fe69e687bfe"},{"sha":"c954bb5600e39f2cc19a96bcbb912ac694b3c16a","author":{"name":"Pierre Letouzey","email":"7f57ef47d7df4bda39ff7662fedf6b8fbea1832c@inria.fr"},"message":"Makefile.install: fix the install of plugin cmi\n\n Now that the plugins are packed, a plugin forms now a unique\n compilation unit, and we only need to install the main cmi file of\n this plugin (foo_plugin.cmi).\n\n Btw, better variable names (e.g. OMEGACMO instead of OMEGACMA) and\n some other cleanup in Makefile.common (no more INITPLUGINS variable,\n for instance).","distinct":false,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/c954bb5600e39f2cc19a96bcbb912ac694b3c16a"},{"sha":"f062b07eea7d06c6a762402e81630b091211d1c6","author":{"name":"Pierre Letouzey","email":"7f57ef47d7df4bda39ff7662fedf6b8fbea1832c@inria.fr"},"message":"Makefile.build: mitigate potential issues with multiple creations of pack .cmi","distinct":false,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/f062b07eea7d06c6a762402e81630b091211d1c6"},{"sha":"3fedd01838fbba1e6d0b79eb41bd26eb1572e303","author":{"name":"Pierre Letouzey","email":"7f57ef47d7df4bda39ff7662fedf6b8fbea1832c@inria.fr"},"message":"remove an old workaround for OCaml 3.11 + MacOS natdynlink","distinct":false,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/3fedd01838fbba1e6d0b79eb41bd26eb1572e303"},{"sha":"31eead537632931d44d31f55905a277d7e5b1624","author":{"name":"Pierre Letouzey","email":"7f57ef47d7df4bda39ff7662fedf6b8fbea1832c@inria.fr"},"message":"Makefile.install: fix a typo in last commit c954bb5, sorry","distinct":false,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/31eead537632931d44d31f55905a277d7e5b1624"},{"sha":"59f2255105922f019be0905d188e638d49053e10","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/59f2255105922f019be0905d188e638d49053e10"},{"sha":"922ad0c1cb4a4badf4c9c2cd098285a008495519","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Removing tactic compatibility layers in setoid_ring.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/922ad0c1cb4a4badf4c9c2cd098285a008495519"},{"sha":"1eea5f0081264ccb01a12f682734e8a624f83804","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimization in the subst tactic.\n\nWe use simple variable substitution instead of full-power term\nmatching.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/1eea5f0081264ccb01a12f682734e8a624f83804"},{"sha":"d5c3569d20253166487482dfb69716985943863c","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimization in the subst tactic.\n\nDo not evar-normalize the term to substitute with. The engine should be\ninsensitive to this kind of modification.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/d5c3569d20253166487482dfb69716985943863c"},{"sha":"f3a39777af60c649ef799fe88c218ce1010f0a5c","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimization in the subst tactic.\n\nDo not normalize all goals beforehand.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/f3a39777af60c649ef799fe88c218ce1010f0a5c"},{"sha":"b8a52d6949f1bc19ad54a08107e846c492eaa850","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimize the clear tactic.\n\nWe do not check for presence of a variable in a global definition when we know\nthat this variable was not present in the section.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/b8a52d6949f1bc19ad54a08107e846c492eaa850"},{"sha":"86da26360d2136e9579beeb59b192ccfb0e67c18","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimize the clear tactic.\n\nWe do not allocate a closure in the main loop, and do so only when needed.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/86da26360d2136e9579beeb59b192ccfb0e67c18"},{"sha":"bd170eb3937aa55f665a671fe9d2916a26af2a09","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimize the subst tactic.\n\nDo not evar-normalize the argument provided by afterHyp.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/bd170eb3937aa55f665a671fe9d2916a26af2a09"},{"sha":"e5446e385ba283f3c4cde83e0fc14987e500778a","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optim in Clenv: use noccurn instead of depends.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/e5446e385ba283f3c4cde83e0fc14987e500778a"},{"sha":"f4f08411e85185cb03ea0ee0cb42c59988015e65","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optmimize the subst tactic.\n\nTake advantage that the provided term is always a variable in Equality.is_eq_x.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/f4f08411e85185cb03ea0ee0cb42c59988015e65"},{"sha":"4d4e2f421c1a4f0339568d3c96ff2459a027aa09","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Optimize the subst tactic.\n\nUse a much dumber algorithm to recognize the shape of equalities.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/4d4e2f421c1a4f0339568d3c96ff2459a027aa09"},{"sha":"a553126c9e0984f38b1a15f2db60458813a177c9","author":{"name":"Pierre-Marie Pédrot","email":"fbe7eee845793c0822ea4e97f0cbb69fd50e1a51@inria.fr"},"message":"Several easy but efficient optimizations for subst and clear tactics.\n\nThey were spotted by profiling tactics manipulating huge terms, provided by\nJason Gross.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/a553126c9e0984f38b1a15f2db60458813a177c9"},{"sha":"c6d9d4fb142ef42634be25b60c0995b541e86629","author":{"name":"Daniel de Rauglaudre","email":"6d27ecba9f15533f00e73482b5fca7d983a6c31f@inria.fr"},"message":"Adding ability to put any pattern in binders, prefixed by a quote.\n\nCf CHANGES for details.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/c6d9d4fb142ef42634be25b60c0995b541e86629"},{"sha":"c1caa158add73e6e6028ade81a0cb4540a845d18","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Merge branch 'funpattern' into trunk. Was PR#142: Binder syntax.","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/c1caa158add73e6e6028ade81a0cb4540a845d18"},{"sha":"cbbc76d0ac6c9710d341b8bc0362aa9d7599f45d","author":{"name":"Arnaud Spiwack","email":"a6a02a54042c1400b77a9dbc2a1b7e9f0dda3490@spiwack.net"},"message":"Patterns in binders: functional tests","distinct":true,"url":"https://api.github.com/repos/letouzey/coq-wip/commits/cbbc76d0ac6c9710d341b8bc0362aa9d7599f45d"}]}
{"actor":{"display_login":"letouzey"}}