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 /parsing/pcoq.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 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f959bd80c..48604e188 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -80,6 +80,8 @@ module type S = (* Get comment parsing information from the Lexer *) val comment_state : coq_parsable -> ((int * int) * string) list + val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit + (* Apparently not used *) val srules' : production_rule list -> symbol val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a @@ -299,6 +301,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b (** Location Utils *) +val of_coqloc : Loc.t -> Ploc.t val to_coqloc : Ploc.t -> Loc.t val (!@) : Ploc.t -> Loc.t |