{"push_id":1124558856,"size":58,"distinct_size":22,"ref":"refs/heads/feature/error_resilience","head":"183aab645f75277a464e4a65d9c2639fe8c0cece","before":"51647f7ec0718ecfc33e832ad4ef51b4d29dd8c9","commits":[{"sha":"4950a69874524dd6d79ca6a83b0c36d6dd1a3e45","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Removing dead code in Compat.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/4950a69874524dd6d79ca6a83b0c36d6dd1a3e45"},{"sha":"9891f2321f13861e3f48ddb28abcd5a77be30791","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Hardening the obsolete unsafe_grammar_statement API.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/9891f2321f13861e3f48ddb28abcd5a77be30791"},{"sha":"6150d15647afc739329019f7e9de595187ecc282","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Removing the Entry module now that rules need not be marshalled.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/6150d15647afc739329019f7e9de595187ecc282"},{"sha":"53724bbcce87da0b1a9a71da4e5334d7a893ba49","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Purer implementation of empty level registering in Pcoq.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/53724bbcce87da0b1a9a71da4e5334d7a893ba49"},{"sha":"946a3d4a800ae1f459cb67cc15c9e6ec44fb3f94","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Simpler data structure for Arules token.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/946a3d4a800ae1f459cb67cc15c9e6ec44fb3f94"},{"sha":"61f79019be6082c3ebabd503c322fb2edb05a99a","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"AlistNsep token now accepts an arbitrary separator.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/61f79019be6082c3ebabd503c322fb2edb05a99a"},{"sha":"810afe7c16ca2d18ac7fb39b1d3bd1a3db1c1331","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Type-safe constr notations.\n\nThis removes the last call to unsafe_grammar_extend, so that all handwritten\ngrammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are\nstill using the unsafe interface, but as they insert explicit casts they are\ndeemed safe.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/810afe7c16ca2d18ac7fb39b1d3bd1a3db1c1331"},{"sha":"b82512946a2818e13397b9f1a128fcafe4a78ba5","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Further tidying of the constr extension code.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/b82512946a2818e13397b9f1a128fcafe4a78ba5"},{"sha":"bc3981687cd363820e35e5a2bd037d50e213f524","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Overlooked use of Gram instead of G module in Pcoq.\n\nThis was probably wreaking havoc in tricky undo-redo scenarii.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/bc3981687cd363820e35e5a2bd037d50e213f524"},{"sha":"f2983cec3544473b18ebc4d4e3a20b941decd196","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Delimiting the use of unsafe code in Pcoq.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/f2983cec3544473b18ebc4d4e3a20b941decd196"},{"sha":"17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Moving the grammar summary to Pcoq.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/17da4a6805622ab3b5e46b0c3ffef57e4b7ded4c"},{"sha":"df2d71323081f8a395881ffc0e1793e429abc3bb","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Turning the grammar extend command API into a state-passing one.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/df2d71323081f8a395881ffc0e1793e429abc3bb"},{"sha":"85753a0bdb6183604a78232c4c32fd15f7a21a2a","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Moving the constr empty entry registering to the state-based API.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/85753a0bdb6183604a78232c4c32fd15f7a21a2a"},{"sha":"16d0e6f7cfc453944874cc1665a0eb4db8ded354","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Making the grammar command extend API purely functional.\n\nInstead of leaving the responsibility of extending the grammar to the caller,\nwe ask for a list of extensions in the return value of the function.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/16d0e6f7cfc453944874cc1665a0eb4db8ded354"},{"sha":"9acfdfd9b7d1cae34b97a4c06c52c4646e15589b","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"The grammar_extend function now registers unsynchronized extensions.\n\nThis made little sense, as all the uses of this function were actually\ncalled from toplevel ML modules. This was at best useless, and at worst\na source of bugs when loading plugins and messing with backtracking.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/9acfdfd9b7d1cae34b97a4c06c52c4646e15589b"},{"sha":"4d9bcbda2fbf09939cddff4e4b42e5397d8a5cf1","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Thorough rewriting of the Pcoq API towards safety and static invariants.\n\nAmongst other things:\n\n1. No more unsafe grammar extensions, except when going through the CAMLPX-based\nPcoq.Gram module. This is mostly safe because CAMLPX adds casts to ensure that\nparsing rules are well-typed. In particular, constr notation is now based on\nGADTs ensuring well-typedness.\n\n2. Less reliance on unsafe coq inside Pcoq, and exposing a self-contained API.\nThe Entry module was also removed as it now results useless.\n\n3. Purely functional API for synchronized grammar extension. This gets rid of\nquite buggy code maintaining a table of empty entries to work around CAMLPX bugs.\nThe state modification is now explicit and grammar extensions synchronized with\nthe summary must provide the rules they want to perform instead of doing so\nimperatively.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/4d9bcbda2fbf09939cddff4e4b42e5397d8a5cf1"},{"sha":"c5de2c3a2aa96c468e7583577141a93e359a9baf","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Fix bug #4722: Coq dies when encountering broken symbolic links.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/c5de2c3a2aa96c468e7583577141a93e359a9baf"},{"sha":"123504209e35b98ac14956ec6950cb7cd8b0089b","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"Small optimization in evar resolution.\n\nInstead of rebuilding a whole set of evars just to make a typeclass filter,\nwe use the source evarmap.","distinct":true,"url":"https://api.github.com/repos/gares/coq/commits/123504209e35b98ac14956ec6950cb7cd8b0089b"},{"sha":"b679eae9d3588f6cb91be174ab80a64fb5c434a4","author":{"email":"d45bbc7219d0bd4f68cd1f2123ca07c7ea74db3e@inria.fr","name":"Pierre-Marie Pédrot"},"message":"More informative error message when interpreting ltac variables in terms.","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/b679eae9d3588f6cb91be174ab80a64fb5c434a4"},{"sha":"bd0befffb80c3086e3b451456cec24f3a12ac1f0","author":{"email":"4f6d07e2b142da7a8716d1cd541ae44f0d273335@inria.fr","name":"Enrico Tassi"},"message":"Dyn: simplify API introducing an Easy submodule\n\nNow the casual Dyn user does not need to be a GADT guru","distinct":false,"url":"https://api.github.com/repos/gares/coq/commits/bd0befffb80c3086e3b451456cec24f3a12ac1f0"}]}
{"actor":{"display_login":"gares"}}