aboutsummaryrefslogtreecommitdiff
path: root/parsing/egramml.mli
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
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
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-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-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-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
2013-06-06More comments in Genarg.ppedrot
2012-12-14Modulification of identifierppedrot
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-14 06:49:31 +0000