diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-19 18:17:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-29 23:02:38 +0200 |
| commit | f99f60902d7492902110fb091c52e58e1ed9cd32 (patch) | |
| tree | 44773647a104546828143de8636a5388b10b3260 /plugins/ltac/tacinterp.mli | |
| parent | e25d69f5d47f7ad6584bf54ea48e42fd482c95e0 (diff) | |
Use a homebrew parser to replace the GEXTEND extension points of Camlp5.
The parser is stupid and the syntax is almost the same as the previous one.
The only difference is that one needs to wrap OCaml code between { braces }
so that quoting works out of the box.
Files requiring such a syntax are handled specifically by the type system
and need to have a .mlg extension instead of a .ml4 one.
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
0 files changed, 0 insertions, 0 deletions