{"push_id":3000221064,"size":114,"distinct_size":1,"ref":"refs/heads/mv-checker-main-coqchk","head":"98a792b79c4bea810bc4fe623c9006e8eeaeb468","before":"f0f45a3f1bf57674e3e24c510aedf65501dcf5c1","commits":[{"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/SkySkimmer/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/SkySkimmer/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/SkySkimmer/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/SkySkimmer/coq/commits/b92700b03904280edf730d02939650b9ac4a9fb6"},{"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/SkySkimmer/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/SkySkimmer/coq/commits/a623c11adac7c34aae92dbeb0c5b7ecc863ce6fd"},{"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/SkySkimmer/coq/commits/f113e4c5ddbc3b13c589b8384120837465af76fa"},{"sha":"62edc7839bb4b534ea0e82d4ed36f504ad04cb16","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"[omega] Remove dead code","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/62edc7839bb4b534ea0e82d4ed36f504ad04cb16"},{"sha":"8bba1951cab1088d057aac68425271191b7c296c","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"[btauto] Remove dead code","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/8bba1951cab1088d057aac68425271191b7c296c"},{"sha":"7af4bcb7003d4f02542834930ad0da1e83c5ff0c","author":{"name":"Vincent Laporte","email":"5b9500d3ac195ca166d1abfbb700bb9943ca7b7b@fondation-inria.fr"},"message":"[Omega] Remove dead code","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/7af4bcb7003d4f02542834930ad0da1e83c5ff0c"},{"sha":"6a7bcfc6d22ab3bf38847fa3fd05ec194187ff50","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Deprecate Global.universes_of_global (replaced by environ version)","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/6a7bcfc6d22ab3bf38847fa3fd05ec194187ff50"},{"sha":"72de7e057505c45cdbf75234a9ea90465d0e19ec","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Simplify fresh_foo_instance functions and pretyping of univ instance","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/72de7e057505c45cdbf75234a9ea90465d0e19ec"},{"sha":"5993c266300cca1c7ca6e8b2b8e3f77f745ca9f9","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Simplify vars_of_global usage","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/5993c266300cca1c7ca6e8b2b8e3f77f745ca9f9"},{"sha":"404291584e861cc0f41a5585280143d2df78bd26","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Remove [constr_of_global_in_context] in funind","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/404291584e861cc0f41a5585280143d2df78bd26"},{"sha":"5bf063c15468bb81f0f48b583f600250cd829aee","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"UnivGen.constr_of_glob_univ -> Constr.mkRef","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/5bf063c15468bb81f0f48b583f600250cd829aee"},{"sha":"5b49e4d674ee2b41206da2d59dc23e4ae2adf388","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Simplify UnivGen.type_of_reference","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/5b49e4d674ee2b41206da2d59dc23e4ae2adf388"},{"sha":"e3615bc48819361891a8d768f5e13eac57a945d0","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Deprecate univ-dropping UnivGen.new_sort_in_family","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/e3615bc48819361891a8d768f5e13eac57a945d0"},{"sha":"bab144fed76c452c49c95c87682d442df68b82f2","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Clean UnivGen.fresh_instance API","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/bab144fed76c452c49c95c87682d442df68b82f2"},{"sha":"da049e138e2b1acf9cdd40d3dbac4508f76f21cb","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Deprecate UnivGen.new_{univ,Type,Type_sort}\n\nThey are impractical since we need to get the level out to register it\nafterwards.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/da049e138e2b1acf9cdd40d3dbac4508f76f21cb"},{"sha":"e99b4c66cf38bb5b6ccb76b69ebd7e7a44ed295d","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"UnivGen.extend_context -> Univ.extend_in_context_set\n\nSuch a basic function can live in Univ rather than the higher level UnivGen.","distinct":false,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/e99b4c66cf38bb5b6ccb76b69ebd7e7a44ed295d"}]}
{"actor":{"display_login":"SkySkimmer"}}