{"push_id":2618682751,"size":534,"distinct_size":4,"ref":"refs/heads/uniform-params-option","head":"2ffc6b74a75b715caf1e8df8ec7116b7eb7c3087","before":"7749c2def9f2223d16c3bc54c024425982acd7aa","commits":[{"sha":"2c7fb44684b26d9c9aea0794b9f0d52088337477","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Fixes #7011 (Fix/CoFix were not considered in tactic unification).","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/2c7fb44684b26d9c9aea0794b9f0d52088337477"},{"sha":"addc553ce5867d25f139bf794752ddcddb5381e7","author":{"name":"Maxime Dénès","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr"},"message":"[default.nix] Unpin nixpkgs\n\nSphinx dependencies are now available in unstable channel","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/addc553ce5867d25f139bf794752ddcddb5381e7"},{"sha":"92526ebd960d2a878b6a1066acc55f0754c4c824","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Fix #6770: fixpoint loses locality info in proof mode.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/92526ebd960d2a878b6a1066acc55f0754c4c824"},{"sha":"ce9b17821a3be3dee7fa7e49c35edaefc658b965","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[lib] Move global options to their proper place.\n\nRecent commits introduced global flags, but these should be\nmodule-specific so relocating.\n\nGlobal flags are deprecated, and for 8.9 `Lib.Flags` will be reduced\nto the truly global stuff.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/ce9b17821a3be3dee7fa7e49c35edaefc658b965"},{"sha":"11fe480932306e3bd702b19674f385f5e36398b7","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Script to identify the code owner for given files\n\nCan be used with git diff --name-only to identify owners for changes\nin given commits.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/11fe480932306e3bd702b19674f385f5e36398b7"},{"sha":"ea1d8bbc3cddbd661439155240bd6f9ec477d84c","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"check-owners.sh: add --show-patterns and --owner options\n\n```bash\n$ dev/tools/check-owners.sh --show-patterns Makefile Makefile.build\n/Makefile*: @letouzey\n\n$ dev/tools/check-owners.sh --owner '@gares' stm/stm.ml interp/declare.ml\nstm/stm.ml: @gares\n\n$ dev/tools/check-owners.sh --show-patterns --owner '@gares' stm/*.ml interp/*.ml\n/stm/: @gares\n```","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/ea1d8bbc3cddbd661439155240bd6f9ec477d84c"},{"sha":"31c04ca25cbb9963d74060746ba57460d98acbfe","author":{"name":"Anton Trunov","email":"102351241e6535e910c45ea1c8a973e34362744c@gmail.com"},"message":"Sphinx docs: clarify strict implicit arguments","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/31c04ca25cbb9963d74060746ba57460d98acbfe"},{"sha":"036a8660f11178a2523982d109ba11b99c062a3d","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Fix #5539: algebraic universe produced by cases.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/036a8660f11178a2523982d109ba11b99c062a3d"},{"sha":"15e43996b342f2eddf0c6c0bd4166e757589337e","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Fixes #7195 (missing freshness condition in Ltac pattern-matching names).\n\nWe ensure that all original names in a spine of matched nested binders\nare distinct.\n\nNote: This enforces that two binders with same internal names are kept\ndisjoint but this does not enforce that we shall respect names exactly\nas they are printed. Only the original prefix of the internal names\nare preserved, not their \"0\" or \"1\" etc. suffix.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/15e43996b342f2eddf0c6c0bd4166e757589337e"},{"sha":"306b45f889f83846b1ab10d3b37d9f3e7817a5db","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Do not compute constr matching context if not used.\n\nThis mitigates bug #6860.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/306b45f889f83846b1ab10d3b37d9f3e7817a5db"},{"sha":"7913b03ba5072efeb9f6ef009ce27cec8ff19cac","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Replace uses of Termops.dependent by more specific functions.\n\nThis is more efficient in general, because Termops.dependent doesn't take\nadvantage of the knowledge of its pattern argument.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/7913b03ba5072efeb9f6ef009ce27cec8ff19cac"},{"sha":"357c94b3e42d4422e311799771f9e28249fc3608","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Adding an overlay for Ltac2.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/357c94b3e42d4422e311799771f9e28249fc3608"},{"sha":"ce2ce8f2c302e538514ecb48b0a8c41bdcb80124","author":{"name":"Hugo Herbelin","email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr"},"message":"Attempt to fix the doubly encapsulated Ltac errors in coqide.\n\nIt seems that ExplainErr.process_vernac_interp_error is called twice\nin CoqIDE. First time in Stm.stm_vernac_interp (via\nStm.call_process_error_once). Second time in the \"handle_exn\" method\nused by CoqIDE to handle exceptions coming from Coq\n(ide_slave.ml/xmlprotocol.ml).\n\nThe proposed fix is to remove the call in CoqIDE, assuming that the\nprocess_vernac_interp_error call is done otherwise on all potential\nerror paths.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/ce2ce8f2c302e538514ecb48b0a8c41bdcb80124"},{"sha":"9ab85ef978c78edb3e4e5ec97ec93a970f021fc2","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"universe minimization: cleanup using standard combinators, open Univ\n\neg Constraint.partition + filter instead of a complicated fold.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/9ab85ef978c78edb3e4e5ec97ec93a970f021fc2"},{"sha":"f53890d1629ea7aaff86ea92e5ac27ab027b2e8d","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"universe normalisation: put equivalence class partition in UGraph\n\nie don't go through having Eq constraints but directly to the unionfind.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/f53890d1629ea7aaff86ea92e5ac27ab027b2e8d"},{"sha":"e6b732d6fbb84d54eb3796e9fa1d10421532f3cd","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"minimize_univ_variables: remove [and right] abbreviation.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/e6b732d6fbb84d54eb3796e9fa1d10421532f3cd"},{"sha":"4baca7221917685210899b766e71782ddae4249f","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"minimize_univ_variables: bool*bool*univ*lowermap replaced by record","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/4baca7221917685210899b766e71782ddae4249f"},{"sha":"bc0246f5a570f70c7befb150d7b544032acbaf7e","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"niv minimization: remove [remove_lower] abbreviation\n\nIt's not long, used only once and it's easier to understand what it\ndoes when it's inlined.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/bc0246f5a570f70c7befb150d7b544032acbaf7e"},{"sha":"998093e64d1eae5ed20900e826a081fac54a9eb9","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"univ minimization: comment compare_constraint_type","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/998093e64d1eae5ed20900e826a081fac54a9eb9"},{"sha":"9384726b851097957a139907907ced72f1ae461b","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"univ minimization: simplify try-with block around [find u left]\n\nThis makes it clear where the Not_found can come from.","distinct":false,"url":"https://api.github.com/repos/jashug/coq/commits/9384726b851097957a139907907ced72f1ae461b"}]}
{"actor":{"display_login":"jashug"}}