{"push_id":2665088117,"size":33,"distinct_size":25,"ref":"refs/heads/fix/ssr/univ-rew","head":"cb81adb6a438fe218e11192b09e085770c7d3067","before":"8827fbbaaa0bfe55531158d275acd4d69aaa2fb4","commits":[{"sha":"ec741e8bb1bdf69f0be4bb6b594560af57f8811c","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"[build] Fix checks and notes noting 4.02.1 instead of 4.02.3\n\nBumping to 4.02.3 was decided some time ago in the WG, however a\ncouple of places escaped updating.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/ec741e8bb1bdf69f0be4bb6b594560af57f8811c"},{"sha":"e82e8e216c4955db58255062fb5c61c7b2aa3c2a","author":{"name":"Matthieu Sozeau","email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr"},"message":"Better elaboration of pattern-matchings on primitive projections\n\nThis ensures that computations are shared as much as possible, mimicking\nthe \"positive\" records computational behavior if possible.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/e82e8e216c4955db58255062fb5c61c7b2aa3c2a"},{"sha":"bc103cc493b2127f8a570bcf2e8be94378d79a55","author":{"name":"Matthieu Sozeau","email":"6890fa1d738eb4a06cf1d2634a31d4aac12540b7@mattam.org"},"message":"Add test-suite case for performance, had to use Timeout","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/bc103cc493b2127f8a570bcf2e8be94378d79a55"},{"sha":"e8daea1c5f0ceb161ea1050698fcc8bb7e7cce17","author":{"name":"Perry E. Metzger","email":"ef248fe27323d9d6d85e87a348c764c793bd79b4@piermont.com"},"message":"Fix #7836: tools/inferior-coq.el uses next-line instead of forward-line.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/e8daea1c5f0ceb161ea1050698fcc8bb7e7cce17"},{"sha":"b22595da96013de18f4a2bab5e6333d75a650554","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Move indexes on top on the TOC. Closes #7764.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/b22595da96013de18f4a2bab5e6333d75a650554"},{"sha":"7f528cdb0ee42a40792d242357a239969f51cada","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Add introduction and credits to the TOC.\n\nMove credits to its own chapter (closes #6573).","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/7f528cdb0ee42a40792d242357a239969f51cada"},{"sha":"61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f","author":{"name":"Maxime Dénès","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr"},"message":"Remove reference name type.\n\nreference was defined as Ident or Qualid, but the qualid type already\npermits empty paths. So we had effectively two representations for\nunqualified names, that were not seen as equal by eq_reference.\n\nWe remove the reference type and replace its uses by qualid.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f"},{"sha":"89a85a6603b7112e685a052d728284d3e4c2881e","author":{"name":"Gaëtan Gilbert","email":"26fa16609af92f7dd138c57814f0f88d569d969c@skyskimmer.net"},"message":"Fix #7421: constr_eq ignores universe constraints.\n\nThe test isn't quite the one in #7421 because that use of algebraic\nuniverses is wrong.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/89a85a6603b7112e685a052d728284d3e4c2881e"},{"sha":"133ac4fbb9a8b4213cb3f8ca2f7c2568931209ce","author":{"name":"Maxime Dénès","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr"},"message":"Overlay for reference removal","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/133ac4fbb9a8b4213cb3f8ca2f7c2568931209ce"},{"sha":"36e38a3768251dbcf20c4de2b746e5eee33da909","author":{"name":"Clément Pit-Claudel","email":"29eb7083085630ded4c2f914c70334cd49eb7bb3@live.com"},"message":"[doc] Use productionlist instead of prodn in ring.rst","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/36e38a3768251dbcf20c4de2b746e5eee33da909"},{"sha":"4687e40504024b51b63bc5681feba13ea6dffbaf","author":{"name":"Clément Pit-Claudel","email":"29eb7083085630ded4c2f914c70334cd49eb7bb3@live.com"},"message":"[doc] Fix uncaught duplicate-label errors in the SSReflect chapter","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/4687e40504024b51b63bc5681feba13ea6dffbaf"},{"sha":"21a0af5b7743e5a1013438210492991b51d878c4","author":{"name":"Clément Pit-Claudel","email":"29eb7083085630ded4c2f914c70334cd49eb7bb3@live.com"},"message":"[doc] Fix a typo in the ssreflect chapter","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/21a0af5b7743e5a1013438210492991b51d878c4"},{"sha":"3d8342c2c26f710583e6b9246bd1069cb8b42d7d","author":{"name":"Clément Pit-Claudel","email":"29eb7083085630ded4c2f914c70334cd49eb7bb3@live.com"},"message":"[doc] Rewrite and document the prodn directive\n\nIt was broken and undocumented. We dropped the git logs, too, so it wasn't clear\nwho wrote it and why it was introduced in the first place.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/3d8342c2c26f710583e6b9246bd1069cb8b42d7d"},{"sha":"a5722cc823dcf13594098dd21813feaaaf893bf0","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/a5722cc823dcf13594098dd21813feaaaf893bf0"},{"sha":"c37881f3d64a6db0d7414eb18adfa4de6b64d4b1","author":{"name":"Pierre-Marie Pédrot","email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr"},"message":"Merge PR #6754: Better elaboration of pattern-matchings on primitive projections","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/c37881f3d64a6db0d7414eb18adfa4de6b64d4b1"},{"sha":"6715e6801c1d285a12eeca55dd8b831d7efb8c0d","author":{"name":"Enrico Tassi","email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr"},"message":"Merge PR #7797: Remove reference name type.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/6715e6801c1d285a12eeca55dd8b831d7efb8c0d"},{"sha":"5122eb4da3691d32483acd3e481c89d9e5c5c5b9","author":{"name":"Maxime Dénès","email":"1d6e1cf70ec6f9ab28d3ea4b27a49a77654d370e@maximedenes.fr"},"message":"[coqtop] Give priority to stdlib load path over current directory\n\nWhen initilazing the load path, coqtop adds implicit bindings for stdlib\nand for the current directory (-R stdlib Coq -R . \"\"). In case of\na clash, the binding of the current directory had priority, which makes\nit impossible to edit stdlib files (when they Require files from the\nsame directory) using PG, or from CoqIDE when launched from the directory\ncontaining the file.\n\nExample to reproduce the problem:\n\n```\ncd plugins/omega\ncoqide Omega.v\n```\n\nsome of the Requires will fail.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/5122eb4da3691d32483acd3e481c89d9e5c5c5b9"},{"sha":"2fc745314f0d2115970fa2d79c4d745b2d27abe4","author":{"name":"Théo Zimmermann","email":"6e6d7530e858430757598f1bcaab6b049abcfdf1@univ-paris-diderot.fr"},"message":"Make Clément the secondary codeowner of doc/tools/coqrst.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/2fc745314f0d2115970fa2d79c4d745b2d27abe4"},{"sha":"3d4899f841adc7cb0c1cec7c49ae3366dda3b217","author":{"name":"Emilio Jesus Gallego Arias","email":"a1debd7f3d9036292773dd21463eb601946b38d8@x80.org"},"message":"Merge PR #7868: [coqtop] Give priority to stdlib load path over current directory","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/3d4899f841adc7cb0c1cec7c49ae3366dda3b217"},{"sha":"5808915bcb5f9800727cc10e5232c8983e1842bd","author":{"name":"Jim Fehrle","email":"bf824f37ce1959e4c2f9e2b389d1c2711164087e@sbcglobal.net"},"message":"On cygwin, pass the filename in a format that coqdoc understands.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/5808915bcb5f9800727cc10e5232c8983e1842bd"}]}
{"actor":{"display_login":"gares"}}