aboutsummaryrefslogtreecommitdiff
path: root/parsing/egramml.ml
AgeCommit message (Expand)Author
2018-05-27[api] [parsing] Move Egram* to `vernac/`Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-16Adding support for using grammar entries returning no value in EXTEND.Hugo Herbelin
2017-04-25[location] Remove `Loc.internal_ghost`Emilio Jesus Gallego Arias
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-06 19:02:16 +0000