aboutsummaryrefslogtreecommitdiff
path: root/parsing/egramml.ml
AgeCommit message (Expand)Author
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-03-19Do not export entry_key from Pcoq anymore.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Remove some useless type declarations.Guillaume Melquiond
2016-01-02Simplification of grammar_prod_item type.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.grammar_prod_item.Pierre-Marie Pédrot
2015-10-27Getting rid of most uses of unsafe_grammar_extend.Pierre-Marie Pédrot
2015-10-27Type-safe Egramml.make_rule.Pierre-Marie Pédrot
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-10-21Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-09-10VernacExtend does not dispatch on type anymore.Pierre-Marie Pédrot
2014-05-12Moving the ML tactic extension mechanism to a Libobject-based one.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-06-21Splitted up Genarg in four different levels:ppedrot
2012-12-14Modulification of identifierppedrot
2012-10-15Egramml: minor simplificationletouzey
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29Split Egrammar into Egramml and Egramcoqletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 01:43:24 +0000