aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrparser.mli
AgeCommit message (Expand)Author
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-02-11[ssreflect] Export more parsing witnesses.Emilio Jesus Gallego Arias
2018-11-26[ssreflect] Export more parsing witnesses.Emilio Jesus Gallego Arias
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias
2018-03-05[ssreflect] Export parsing witnesses in mli file.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-25[api] Remove type equalities from API.Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-06-07Put "ssreflect" behind "API".Matej Košík
2017-06-06Merge the ssr plugin.Maxime Dénès