aboutsummaryrefslogtreecommitdiff
path: root/gramlib/dune
AgeCommit message (Collapse)Author
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
This introduces a bit of noise in the Dune files but for now I think it is the best way to do it.
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`