diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-27 11:44:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-27 14:02:49 +0100 |
| commit | 72bed859fb8d037044abd8a1518661c52502f7be (patch) | |
| tree | a338b6d023c32db4f7cf0226117ab2f33b5dbca6 /grammar/vernacextend.ml4 | |
| parent | d51e5688f521c8a77a1dbdb0b88d8f99d5ff8060 (diff) | |
Type-safe Egramml.grammar_prod_item.
Diffstat (limited to 'grammar/vernacextend.ml4')
| -rw-r--r-- | grammar/vernacextend.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 5d4309aba..54638556d 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -35,6 +35,7 @@ type rule = { let rec make_let e = function | [] -> e | GramNonTerminal(loc,t,_,Some p)::l -> + let t = Genarg.unquote t in let loc = of_coqloc loc in let p = Names.Id.to_string p in let loc = CompatLoc.merge loc (MLast.loc_of_expr e) in @@ -182,10 +183,10 @@ EXTEND args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let EntryName (t, g) = interp_entry_name false TgAny e "" in - GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s)) + GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> let EntryName (t, g) = interp_entry_name false TgAny e sep in - GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s)) + GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) | s = STRING -> GramTerminal s ] ] |