aboutsummaryrefslogtreecommitdiff
path: root/gramlib/plexing.ml
AgeCommit message (Collapse)Author
2018-11-06Removing dead code in Plexing.Pierre-Marie Pédrot
It was full with utility functions and wrappers that are unused in the Coq codebase.
2018-10-29[camlp5] Fix warnings, switch Coq to vendored library.Emilio Jesus Gallego Arias
2018-10-29[camlp5] Automatic conversion from revised syntax + parsersEmilio Jesus Gallego Arias
`for i in *; do camlp5r pr_o.cmo $i > ../gramlib.auto/$i; done`
2018-10-29[gramlib] Original Import from Camlp5 repos.Emilio Jesus Gallego Arias