{"push_id":883267716,"size":10,"distinct_size":1,"ref":"refs/heads/trunk","head":"e98d3c3793f26265a49f63a6e78d704f88341df9","before":"103ec7205d9038f1f3821f9287e3bb0907a1e3ec","commits":[{"sha":"566a24e28924ad4a7dda99891dce3882e6db112c","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Adding the Printing Projections options to the index.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/566a24e28924ad4a7dda99891dce3882e6db112c"},{"sha":"11ccb7333c2a82d59736027838acaea2237e2402","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"Make the pretty printer resilient to incomplete nametab (progress on #4363).\n\nThe nametab in which the error message is printed is not the one in\nwhich the error message happens.\n\nThis reveals a weakness in the fix_exn code: the fix_exn function should\nbe pure, while in some cases (like this one) uses the global state (the\nnametab) to print a term in a pretty way (the shortest non-ambiguous name\nfor constants).\n\nThis patch makes the externalization phase (used by term printing)\nresilient to an incomplete nametab, so that printing a term in the\nwrong nametab does not mask the original error.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/11ccb7333c2a82d59736027838acaea2237e2402"},{"sha":"982460743a54ecfab1d601ba930d61c04972d17a","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Fixing the \"parsing rules with idents later declared as keywords\" problem.\n\nThe fix was actually elementary. The lexer comes with a function to\ncompare parsed tokens against tokens of the parsing rules. It is\nenough to have this function considering an ident in a parsing rule to\nbe equal to the corresponding string parsed as a keyword.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/982460743a54ecfab1d601ba930d61c04972d17a"},{"sha":"8297baa98147f78263126b1bd6cf41b0456f177d","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"Fix [Polymorphic Hint Rewrite].","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/8297baa98147f78263126b1bd6cf41b0456f177d"},{"sha":"a0e72610a71e086da392c8563c2eec2e35211afa","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"Avoid recording spurious Set <= Top.i constraints which are always\nvalid (when Top.i is global and hence > Set).","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/a0e72610a71e086da392c8563c2eec2e35211afa"},{"sha":"4a11dc25938f3f009e23f1e7c5fe01b2558928c3","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"Univs: entirely disallow instantiation of polymorphic constants with\nProp levels.\n\nAs they are typed assuming all variables are >= Set now, and this was\nbreaking an invariant in typing. Only one instance in the standard\nlibrary was used in Hurkens, which can be avoided easily. This also\navoids displaying unnecessary >= Set constraints everywhere.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/4a11dc25938f3f009e23f1e7c5fe01b2558928c3"},{"sha":"90fef3ffd236f2ed5575b0d11a47185185abc75b","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"Univs: correctly register universe binders for lemmas.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/90fef3ffd236f2ed5575b0d11a47185185abc75b"},{"sha":"15aeb84a0deb444af81f4035dbcf791566bafe5f","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"Closed bugs.","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/15aeb84a0deb444af81f4035dbcf791566bafe5f"},{"sha":"8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56","author":{"email":"ac29333de02e6393d1304388a3accb7dd81e38d4@inria.fr","name":"Matthieu Sozeau"},"message":"Test-suite files for closed bugs","distinct":false,"url":"https://api.github.com/repos/coq/coq/commits/8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56"},{"sha":"e98d3c3793f26265a49f63a6e78d704f88341df9","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Merge branch 'v8.5'","distinct":true,"url":"https://api.github.com/repos/coq/coq/commits/e98d3c3793f26265a49f63a6e78d704f88341df9"}]}