aboutsummaryrefslogtreecommitdiff
path: root/coqpp/coqpp_lex.mll
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
2019-06-17Update headers of files that were stuck on older headers.Théo Zimmermann
2019-06-04Alternate syntax for ![]: VERNAC EXTEND Foo STATE proofGaëtan Gilbert
2019-03-27[coqpp] [ltac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2018-11-02coqpp VERNAC EXTEND uses #[ att = attribute; ] syntaxGaëtan Gilbert
2018-10-15Implement ARGUMENT EXTEND in coqpp.Pierre-Marie Pédrot
2018-10-02Handling VERNAC EXTEND in coqpp.Pierre-Marie Pédrot
2018-10-01Store locations of OCaml quotations in coqpp.Pierre-Marie Pédrot
2018-09-06coqpp: allow DEPRECATED when declaring tacticsVincent Laporte
2018-07-11[coqpp] Move to its own directory.Emilio Jesus Gallego Arias