{"push_id":2137849209,"size":4,"distinct_size":3,"ref":"refs/heads/master+some-fix-ltac-printing+refined-printers","head":"7311c11c52f96670eb6424d27e448c051807f9f5","before":"2e4dd8ec02144bd415267806c4815338e5d1d789","commits":[{"sha":"a83c37de529f12348cd9e3a66a38c58b72777478","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixes #5787 (printing of \"constr:\" lost in the move of constr to Generic).\n\nWas broken since 8.6.","distinct":false,"url":"https://api.github.com/repos/herbelin/github-coq/commits/a83c37de529f12348cd9e3a66a38c58b72777478"},{"sha":"04f973b4db5326f6cd709790da657cee4c758af0","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Fixes #5787 (printing of \"constr:\" lost in the move of constr to Generic).\n\nWas broken since 8.6.","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/04f973b4db5326f6cd709790da657cee4c758af0"},{"sha":"2a0af8a054b8d78197cedba065161d82bfa74651","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Printing again \"intros  **\" as \"intros\" by default.\n\nThe rationale it that it is more common to do so and thus more\n\"natural\" (principle of writing less whenever possible).","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/2a0af8a054b8d78197cedba065161d82bfa74651"},{"sha":"7311c11c52f96670eb6424d27e448c051807f9f5","author":{"name":"Hugo Herbelin","email":"785e2cbe854d07e62ab9406d6852942772342316@inria.fr"},"message":"Extending further PR#6047 (system to register printers for Ltac values).\n\nWe generalize the possible use of levels to raw and glob printers.\n\nThis is potentially useful for printing ltac expressions which are the\nglob level.","distinct":true,"url":"https://api.github.com/repos/herbelin/github-coq/commits/7311c11c52f96670eb6424d27e448c051807f9f5"}]}
{"actor":{"display_login":"herbelin"}}