aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/extraargs.mlg
AgeCommit message (Expand)Author
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2018-12-11[api] Move reduction modules to `tactics`Emilio Jesus Gallego Arias
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot