{"push_id":775361706,"size":25,"distinct_size":25,"ref":"refs/heads/coqide-richpp","head":"59f7e1d3b8e215fef8c9aba4bb3ac8603a380fa1","before":"193bbeaf0a1ada558c276f4e70646f6e256f5f79","commits":[{"sha":"5cec38e8a2fbe39c75404f249974227afc028f27","author":{"email":"20053a48688cff52b9d62b07b361c9ccc1cfc644@cs.harvard.edu","name":"Gregory Malecha"},"message":"report the full module path when reporting errors in coqdep","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/5cec38e8a2fbe39c75404f249974227afc028f27"},{"sha":"8e3c2182d0c43530fc2cf62e63f5474773d04604","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Fixing richpp behaviour w.r.t. its specification.\n\nContrarily to what was described in the API, nodes without annotations\nwere not ignored by the printer but left there instead.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/8e3c2182d0c43530fc2cf62e63f5474773d04604"},{"sha":"2c1882815e7877bfc574f9f71eff6ce099145df5","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Statically ensure that we omit null annotations in Richpp.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/2c1882815e7877bfc574f9f71eff6ce099145df5"},{"sha":"98618cfb6b326b70da29348bc5d212e41086f473","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"More parametric type for generalized XML.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/98618cfb6b326b70da29348bc5d212e41086f473"},{"sha":"54fb2cdf7bb5c45f5a237b2559fd26d90d8f4df1","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"More invariants in Richpp.\n\nWe ensure statically by typing that the tags used by the rich printer\nare integers. Furthermore, we also expose through typing that tags are\nirrelevants in the returned XML.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/54fb2cdf7bb5c45f5a237b2559fd26d90d8f4df1"},{"sha":"2f5bc3148579ff359f179c758a7f4e724a14adf7","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Revert the four previous commits and update the description of Richpp.\n\nCorrecting the code w.r.t. to the API was not the right solution. Instead,\nthe API comment had to be corrected.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/2f5bc3148579ff359f179c758a7f4e724a14adf7"},{"sha":"45779d74209a728cfd67628eaa53b42fee129f65","author":{"email":"43f1ac15e1612ec31474d70389158936df20a6d4@inria.fr","name":"Guillaume Melquiond"},"message":"Remove generatable documentation files from repository. (Fix bug #4315)","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/45779d74209a728cfd67628eaa53b42fee129f65"},{"sha":"369a0c9354497639d96ba2fef94c920e051d00fb","author":{"email":"43f1ac15e1612ec31474d70389158936df20a6d4@inria.fr","name":"Guillaume Melquiond"},"message":"Remove duplicate code.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/369a0c9354497639d96ba2fef94c920e051d00fb"},{"sha":"8a22b549e61a1fc120b20a5b220764df6c49b3f8","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"windows build scripts made more accurate in detecting failures","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/8a22b549e61a1fc120b20a5b220764df6c49b3f8"},{"sha":"00f333fe7ae2e7bd4ced4be78d24737e62a7b369","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Highlighting of the \"Next Obligation\" command in CoqIDE.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/00f333fe7ae2e7bd4ced4be78d24737e62a7b369"},{"sha":"3696238f8dd435426080ba7d1b40c8ceacacb6ee","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Documentation by giving a name to a large type.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/3696238f8dd435426080ba7d1b40c8ceacacb6ee"},{"sha":"15e6e2d666252cad3c1e0de4622ef51c2830b6b8","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Removing code duplication in Lemmas.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/15e6e2d666252cad3c1e0de4622ef51c2830b6b8"},{"sha":"081a649157d2460c924404cd51b4ba50c23b1956","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Fixing #4318 (anomaly when applying args to a recursive notation in patterns).\n\nI don't know what was the intent of Pierre B here. In 8.4, it was not\nsupported, raising with an error at parsing time. I changed the\nanomaly into an error at interpretation time, so it is still not\nsupported but we could support it if some legitimate use of it\neventually appears.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/081a649157d2460c924404cd51b4ba50c23b1956"},{"sha":"2903ee1394118106f1894798f82dc5cf3730675b","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Merge branch 'v8.5'","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/2903ee1394118106f1894798f82dc5cf3730675b"},{"sha":"da8fa23acd4754f025131be846d8036a20009f99","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Allowing the abstract tactical to clear the environment from unused variables.\n\nGrants wish #2098.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/da8fa23acd4754f025131be846d8036a20009f99"},{"sha":"bfbb9f063434623d7c3dac8aa4aaf64c4ec84373","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Documenting the Shrink Abstract option.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/bfbb9f063434623d7c3dac8aa4aaf64c4ec84373"},{"sha":"20ae742e391a8db65e203213a124126ce8621fe1","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Replacing old-style preferences in CoqIDE.\n\nThere is no remaining global preference record anymore, every preference\nis now defined in the new event-based style.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/20ae742e391a8db65e203213a124126ce8621fe1"},{"sha":"c11f4428dbed786fafb90bb1ea8c017867d3e91e","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Fixing generation of dev/printers.mllib.d after ocamllibdep is used (48d611ff2a).","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/c11f4428dbed786fafb90bb1ea8c017867d3e91e"},{"sha":"f1ecbf5014dac5a1bfbd4a5bb352fe303280e44b","author":{"email":"6c2d20c0261809f41f8166782e00714227562ada@inria.fr","name":"Hugo Herbelin"},"message":"Adding a proof of surjective pairing on vectors.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/f1ecbf5014dac5a1bfbd4a5bb352fe303280e44b"},{"sha":"c53f2f75375dfffd2f258c76f5b722d37ab0daf9","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Switching to an event-based mechanism for CoqIDE preferences.\n\nThere is no remaining hook in the preferences. In particular, the\nrefresh_editor_hook is gone.","distinct":true,"url":"https://api.github.com/repos/ppedrot/coq/commits/c53f2f75375dfffd2f258c76f5b722d37ab0daf9"}]}