aboutsummaryrefslogtreecommitdiff
path: root/vernac/metasyntax.mli
AgeCommit message (Expand)Author
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Hugo Herbelin
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias