{"push_id":3024468373,"size":278,"distinct_size":1,"ref":"refs/heads/dune+bootstrap","head":"3ffe9f32f59a967a591889a6c3935fb052d79499","before":"22107b4a304996e2cb890e293174298669719dd9","commits":[{"sha":"86d08ece4c63e2a42f72ddd3afc51ce04cd1932a","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Fix an algorithmic issue in the vernac guardedness checker.\n\nCalling the O(n) EConstr.to_constr function at every node is a very bad\nidea (tm).","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/86d08ece4c63e2a42f72ddd3afc51ce04cd1932a"},{"sha":"60fe31e2424383abaa6c7a86aa65a76bbbc7eff3","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Fix nativenorm when an evar is in the wrong place.\n\nSee commit [Simplify code for [Definition := Eval ...]] which without\nthis breaks test suite 7631.v","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/60fe31e2424383abaa6c7a86aa65a76bbbc7eff3"},{"sha":"c70cc62e74341ccda9a67fccdefb03f6d122406c","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Simplify code for [Definition := Eval ...]\n\nNote that since this now reduces before restricting universes\nbehaviour may be a bit different.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/c70cc62e74341ccda9a67fccdefb03f6d122406c"},{"sha":"1af17614793bfcdaa73afc9965db7fd3918bdc1c","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Stupid but critical unfolding heuristic.\n\nWe favour unfolding of variables over constants because it is more frequent\nfor the former to depend on the latter. This has huge consequences on a few\nextremely slow lines in mathcomp, up to dividing by 3 single-line invocations\nthat were taking about 30s on my laptop before the patch.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/1af17614793bfcdaa73afc9965db7fd3918bdc1c"},{"sha":"2f2d31d8408b4e15b193110309c4800a456cfb83","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"The cbv reduction does not rely on the kernel info data structure anymore.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/2f2d31d8408b4e15b193110309c4800a456cfb83"},{"sha":"e2141cc741c2a77f05dabd9a8b48d9051d6d6cd4","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Clean up CClosure code.\n\nWe take advantage of the separation of implementation from CBV to remove\nconstant code.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/e2141cc741c2a77f05dabd9a8b48d9051d6d6cd4"},{"sha":"b92700b03904280edf730d02939650b9ac4a9fb6","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Also clean up the checker w.r.t. unused closure data.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/b92700b03904280edf730d02939650b9ac4a9fb6"},{"sha":"0a4aaf590100ad9004ed15c5cc1d93a84dee6f50","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[ci] [appveyor] Enable cache for builds.\n\nWe cache CYGWIN and OPAM. Current cygwin install is not deterministic\nbut should do the job in the scope of this job.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/0a4aaf590100ad9004ed15c5cc1d93a84dee6f50"},{"sha":"c4d3daaeb75a746b2a2717d2aaf21a65ebcc7775","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Adding a functional version of constant_of_delta_kn.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/c4d3daaeb75a746b2a2717d2aaf21a65ebcc7775"},{"sha":"23fc1c59d78ffb524265caa1908503f50816335a","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"A state-free version of is_polymorphic.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/23fc1c59d78ffb524265caa1908503f50816335a"},{"sha":"09c63ec6ec76ffbae85a07f7b5c8da692bdcb8b9","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[ci] [appveyor] Disable validate target.\n\nNot a big point on running the checker on Appveyor I think, this will\nsave a bunch of time and improve reliability.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/09c63ec6ec76ffbae85a07f7b5c8da692bdcb8b9"},{"sha":"a623c11adac7c34aae92dbeb0c5b7ecc863ce6fd","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Moving local copy fold_constr_with_full_binders in assumptions.ml to constr.ml.\n\nThis is to move a standard combinator to the place it belongs to. An\nalternative could have been to put it in termops.ml, but termops.ml is\nnow about econstr, so, even if it makes the kernel \"bigger\", constr.ml\nseems to be the best place for this combinator. After all, this\ncombinator is canonical.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/a623c11adac7c34aae92dbeb0c5b7ecc863ce6fd"},{"sha":"697a59de8a39f3a4b253ced93ece1209b7f0eb1b","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Merge PR #8695: Adding a functional version of constant- and mind_of_delta_kn + functional version of is_polymorphic","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/697a59de8a39f3a4b253ced93ece1209b7f0eb1b"},{"sha":"f113e4c5ddbc3b13c589b8384120837465af76fa","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Document the issue with positive coinductive types.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/f113e4c5ddbc3b13c589b8384120837465af76fa"},{"sha":"28127d3bb4a0e151820e04a3efc4846ababb7d71","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"[nsatz] remove dead code","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/28127d3bb4a0e151820e04a3efc4846ababb7d71"},{"sha":"1018c2c749fba12790d623a5889da91453dddabb","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"[micromega] remove dead code","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/1018c2c749fba12790d623a5889da91453dddabb"},{"sha":"ee725c692b3c647eb5f6b29f1330aa2a03219b28","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"[test-suite] Update csdp cache","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/ee725c692b3c647eb5f6b29f1330aa2a03219b28"},{"sha":"33c93006b7685092b5239ea001058578fac3552f","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[clib] Deprecate string functions available in OCaml 4.05\n\n- `CString.strip -> String.trim`\n- `CString.split -> String.split_on_char`\n\nAs noted by @ppedrot there are some small differences on semantics:\n\n> OCaml's `trim` also takes line feeds (LF) into account. Similarly,\n> OCaml's `split` never returns an empty list whereas Coq's `split`\n> does on the empty string.","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/33c93006b7685092b5239ea001058578fac3552f"},{"sha":"50d6f112ca2720e390ef7bdea79d40f9e6119cd5","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[clib] Remove Array functions available in OCaml 4.05.0","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/50d6f112ca2720e390ef7bdea79d40f9e6119cd5"},{"sha":"096d4dd94ff6d506e7a3785da453c21874611cec","author":{"name":"thery","email":"f31fd24ec5d9ab5262f8cc7614d998caa136d4ff@sophia.inria.fr"},"message":"Merge PR #8691: Remove some dead code in nsatz and micromega plugins","distinct":false,"url":"https://api.github.com/repos/ejgallego/coq/commits/096d4dd94ff6d506e7a3785da453c21874611cec"}]}
{"actor":{"display_login":"ejgallego"}}