diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-18 00:32:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-18 01:24:58 +0100 |
| commit | 1730369cd4f7b62a076c93b2a0ece190ee08f7eb (patch) | |
| tree | 31319000fda0d9c98753c490bda9cdf8f3ea80d1 /grammar/argextend.ml4 | |
| parent | b5f6eb57a480d705be9362067e2fb887533c822c (diff) | |
Making the EXTEND macros almost self-contained.
Diffstat (limited to 'grammar/argextend.ml4')
| -rw-r--r-- | grammar/argextend.ml4 | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index f26a66a12..5bf7b65d7 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -10,10 +10,8 @@ open Genarg open Q_util -open Egramml open Compat open Extend -open Pcoq let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> @@ -36,17 +34,10 @@ let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >> let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >> let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >> -let has_extraarg l = - let check = function - | ExtNonTerminal(ExtraArgType _, _, _) -> true - | _ -> false - in - List.exists check l - let make_act loc act pil = let rec make = function | [] -> <:expr< (fun loc -> $act$) >> - | ExtNonTerminal (t, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> + | ExtNonTerminal (_, _, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >> | ExtTerminal _ :: tl -> <:expr< (fun _ -> $make tl$) >> in make (List.rev pil) @@ -241,10 +232,7 @@ EXTEND | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let e = parse_user_entry e sep in ExtNonTerminal (type_of_user_symbol e, e, s) - | s = STRING -> - if String.length s > 0 && Util.is_letter s.[0] then - Lexer.add_keyword s; - ExtTerminal s + | s = STRING -> ExtTerminal s ] ] ; entry_name: |