aboutsummaryrefslogtreecommitdiff
path: root/gramlib/dune
AgeCommit message (Collapse)Author
2018-11-30[gramlib] Remove `Ploc.t` in favor of `Loc.t`Emilio Jesus Gallego Arias
The types are identical and we have no more reason for the split. Note the following TODOS: - discrepancy of `Ploc.after` with `CLexer.after` - discrepancy of `Ploc.comments` with `CLexer.comments` - `Ploc.dummy` vs `Loc.t option`
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`