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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index cc9be7b0e..48f225f97 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -274,7 +274,7 @@ let make_sep_rules = function Arules [r] let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p assoc from forpat -> - if is_binder_level from p then Aentryl (target_entry forpat, 200) + if is_binder_level from p then Aentryl (target_entry forpat, "200") else if is_self from p then Aself else let g = target_entry forpat in @@ -282,7 +282,7 @@ let symbol_of_target : type s. _ -> _ -> _ -> s target -> (s, s) symbol = fun p begin match lev with | None -> Aentry g | Some None -> Anext - | Some (Some (lev, cur)) -> Aentryl (g, lev) + | Some (Some (lev, cur)) -> Aentryl (g, string_of_int lev) end let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun assoc from typ -> match typ with @@ -291,7 +291,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as Alist1 (symbol_of_target typ' assoc from forpat) | TTConstrList (typ', tkl, forpat) -> Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl) -| TTPattern p -> Aentryl (Constr.pattern, p) +| TTPattern p -> Aentryl (Constr.pattern, string_of_int p) | TTClosedBinderList [] -> Alist1 (Aentry Constr.binder) | TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) | TTName -> Aentry Prim.name @@ -428,6 +428,7 @@ let prepare_empty_levels forpat (pos,p4assoc,name,reinit) = let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list = fun level r -> match r with | Stop -> [] | Next (rem, Aentryl (_, i)) -> + let i = int_of_string i in let rem = pure_sublevels level rem in begin match level with | Some j when Int.equal i j -> rem |