{"push_id":1575869847,"size":136,"distinct_size":2,"ref":"refs/heads/kernel-stack-experiments","head":"d11eafb77a3c6564e0a5a8e2d768d9ddbda03a61","before":"940f2851537fcfb097e4ea134b34f00aa3884071","commits":[{"sha":"9907e296e21fdd9dc3fab2b84fe7159b35af654c","author":{"name":"Guillaume Melquiond","email":"66cbeafd26a5b3e38ef65c4d3af3539c02336b4f@inria.fr"},"message":"Remove tabulation support from pretty-printing.\n\nThis mechanism relied on functions that are deprecated in recent versions\nof ocaml. It was incorrectly used for the most part anyway. The only place\nthat was using tabulations correctly is \"print_loadpath\", so there is a\nminor regression there: physical paths of short logical paths are no longer\naligned.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/9907e296e21fdd9dc3fab2b84fe7159b35af654c"},{"sha":"970bd8e901267916ae23bbe661d05c7d64f60b48","author":{"name":"Arnaud Spiwack","email":"a6a02a54042c1400b77a9dbc2a1b7e9f0dda3490@spiwack.net"},"message":"Sort search results by relevance\n\nThis orders the results of search commands (such as `Search`,\n`SearchAbout`, …) according to a \"relevance\" metric to minimise.\n\nIn this minimal version, the metric is the size of the displayed term.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/970bd8e901267916ae23bbe661d05c7d64f60b48"},{"sha":"e0e52953a7b06b52603eb6f592dbf40cb325a4de","author":{"name":"Arnaud Spiwack","email":"a6a02a54042c1400b77a9dbc2a1b7e9f0dda3490@spiwack.net"},"message":"Refine the relevance measure\n\nHaving more disctinc symbols incurs a penalty.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/e0e52953a7b06b52603eb6f592dbf40cb325a4de"},{"sha":"890e0738000d6f12d51761a315b0dd09a915b6c9","author":{"name":"Arnaud Spiwack","email":"a6a02a54042c1400b77a9dbc2a1b7e9f0dda3490@spiwack.net"},"message":"Ordering search: memoise relevance metric\n\nRecalculating the metric all the time was proving costly (it was obvious\neven on small queries).","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/890e0738000d6f12d51761a315b0dd09a915b6c9"},{"sha":"a79a62c9fb5690ff1043d9c0dd44f61cd535cc12","author":{"name":"Arnaud Spiwack","email":"a6a02a54042c1400b77a9dbc2a1b7e9f0dda3490@spiwack.net"},"message":"tclDISPATCH: more informative error message\n\n\"expected _n_ tactics\" -> \"exected _n_ tactics, was given _k_\".\n\nAlso affect other similar tacticals from `Proofview`.\n\nI used that for debugging once, I thought I might as well propose it for\nmergeing.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/a79a62c9fb5690ff1043d9c0dd44f61cd535cc12"},{"sha":"5da573031d36c5a1df5dcf64cc8764f489f774f7","author":{"name":"CJ Bell","email":"2b379b9f53e9c0072e35cbfc958e0285fc920f64@gmail.com"},"message":"Remove unused feedback_content: Goals","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/5da573031d36c5a1df5dcf64cc8764f489f774f7"},{"sha":"ac9f2b1a5789964b1d881d024912350a7506a0f9","author":{"name":"Emilio Jesus Gallego Arias","email":"74bd03b9fa5ba9425c7ecadbbbb4d58aa6999825@x80.org"},"message":"[pp] Set printing width for richpp formatter (bug #5244)\n\nRichpp output depends on printing width, thus its internal formatter\nshould be seeded with the proper width value.\n\nWhile we are at it, we increase the default buffer size to a more\nsensible value.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/ac9f2b1a5789964b1d881d024912350a7506a0f9"},{"sha":"80bd0e81305abfc76831ff1c8361e01c4aabb68e","author":{"name":"Enrico Tassi","email":"a46adc9faf082e84480f72ffaaa22ae593009461@inria.fr"},"message":"ssrmatching: fix iter_constr_LR iterator wrt Proj","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/80bd0e81305abfc76831ff1c8361e01c4aabb68e"},{"sha":"04c3f08807e341273919556652525f8226e94b6d","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"A few words in CHANGES.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/04c3f08807e341273919556652525f8226e94b6d"},{"sha":"7037e2972828f395962284848ce167545253d910","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Set version number to 8.6rc1.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/7037e2972828f395962284848ce167545253d910"},{"sha":"b802f1789b59a93bb84783125f61794c00d6c940","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Add bat files for 8.6beta1 build.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/b802f1789b59a93bb84783125f61794c00d6c940"},{"sha":"fddf3ca8f2499c14018c13417346c567971c0a23","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Add bat files for 8.6rc1 build.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/fddf3ca8f2499c14018c13417346c567971c0a23"},{"sha":"d24aaa4d0e45dc3ec31c5f576516b01ded403dd8","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Commit bumping the version number was partial...\n\nThe sad part of the story is that the script testing this version number\nis run after tagging by the coq-dev-tools Makefile... will fix that.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/d24aaa4d0e45dc3ec31c5f576516b01ded403dd8"},{"sha":"fb637d483d3637f0cf81eed92467f1ff491add2a","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Fix paths in 32-bit windows build scripts.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/fb637d483d3637f0cf81eed92467f1ff491add2a"},{"sha":"fbde1bb856527cc152cd7daf99b85a8c76991a23","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Windows build scripts for 8.6 final.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/fbde1bb856527cc152cd7daf99b85a8c76991a23"},{"sha":"0d1438851ba3a0b9f76847abc42f3bf8ad26c4cb","author":{"name":"Maxime Dénès","email":"3b8e10480754ba93523db5dc4626a5f001e54bb7@maximedenes.fr"},"message":"Set version to 8.6 in configure.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/0d1438851ba3a0b9f76847abc42f3bf8ad26c4cb"},{"sha":"90b61424761c5ba1ddbecf20c29d78b485584ae7","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"Extend Fast_typeops to be a replacement for Typeops\n\nThis brings the fix in cad44fc for #2996 to the copy of\nFast_typeops.check_hyps_inclusion.\n\nFast_typeops.constant_type checks the universe constraints instead of\noutputting them. Since everyone who used Typeops.constant_type just\ndiscarded the constraints they've been switched to constant_type_in\nwhich should be the same in Fast_typeops and Typeops.\n\nThere are some small differences in the interfaces:\n- Typeops.type_of_projection <->\n  Fast_typeops.type_of_projection_constant to avoid collision with the\n  internally used type_of_projection (which gives the type of [Proj(p,c)]).\n- check_hyps_inclusion takes [('a -> constr)] and ['a] instead of\n  [constr] for reporting errors.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/90b61424761c5ba1ddbecf20c29d78b485584ae7"},{"sha":"421d846d80c19226ba0922ff3c3b0006c98c21b6","author":{"name":"Gaetan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@ens-lyon.fr"},"message":"Replace Typeops by Fast_typeops\n\nThis is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial\nchanges in the other files, the real changes are in the parent commit.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/421d846d80c19226ba0922ff3c3b0006c98c21b6"},{"sha":"42f27beb63a629dcef514abb0b31dea193f35a38","author":{"name":"Guillaume Melquiond","email":"66cbeafd26a5b3e38ef65c4d3af3539c02336b4f@inria.fr"},"message":"Fix incorrect documentation that prevents successful compilation (bug #5265).","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/42f27beb63a629dcef514abb0b31dea193f35a38"},{"sha":"c793d102df3e007d824e79f499e71823207c301a","author":{"name":"Guillaume Melquiond","email":"66cbeafd26a5b3e38ef65c4d3af3539c02336b4f@inria.fr"},"message":"Avoid concurrent runs when producing html documentation (bug #5269).\n\nMake does not allow for rules that produce multiple outputs (unless they\nare pattern rules). As a consequence, the hacha rule could be run several\ntimes concurrently, thus causing doc/refman/html to be deleted under the\nfeet of some runs.\n\nThis commit fixes the issue by turning the rule into a single-output rule\nand adding a dummy rule to handle all the other indexes. Note that this is\nnot a perfect solution since, if the user were to manually delete one of\nthe auxiliary index, it would not be rebuilt until the main index is.","distinct":false,"url":"https://api.github.com/repos/psteckler/coq/commits/c793d102df3e007d824e79f499e71823207c301a"}]}
{"actor":{"display_login":"psteckler"}}