diff options
| author | Pierre-Marie Pédrot | 2015-10-27 11:44:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-27 12:40:01 +0100 |
| commit | d51e5688f521c8a77a1dbdb0b88d8f99d5ff8060 (patch) | |
| tree | 3fa5d830feb50a5f96e07c6c4762ac8c3f461189 /grammar | |
| parent | 73c3dddc94dda003b1bb854d3b6ca9d15474e299 (diff) | |
Finer type for Pcoq.interp_entry_name.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 12 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 8 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 8 |
3 files changed, 14 insertions, 14 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 51949e8aad..cfabd26889 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -280,8 +280,8 @@ EXTEND | e = argtype; LIDENT "option" -> OptArgType e ] | "0" [ e = LIDENT -> - let EntryName (t, _) = interp_entry_name false None e "" in - t + let EntryName (t, _) = interp_entry_name false TgAny e "" in + Genarg.unquote t | "("; e = argtype; ")" -> e ] ] ; argrule: @@ -289,11 +289,11 @@ EXTEND ; genarg: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let EntryName (t, g) = interp_entry_name false None e "" in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let EntryName (t, g) = interp_entry_name false TgAny e "" in + GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let EntryName (t, g) = interp_entry_name false None e sep in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let EntryName (t, g) = interp_entry_name false TgAny e sep in + GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s)) | s = STRING -> if String.length s > 0 && Util.is_letter s.[0] then Lexer.add_keyword s; diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 2c9a73a371..8c2a45bae3 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -261,11 +261,11 @@ EXTEND ; tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let EntryName (t, g) = interp_entry_name false None e "" in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let EntryName (t, g) = interp_entry_name false TgAny e "" in + GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let EntryName (t, g) = interp_entry_name false None e sep in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let EntryName (t, g) = interp_entry_name false TgAny e sep in + GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s)) | s = STRING -> if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal."); GramTerminal s diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index f0fde2bf84..5d4309aba0 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -181,11 +181,11 @@ EXTEND ; args: [ [ e = LIDENT; "("; s = LIDENT; ")" -> - let EntryName (t, g) = interp_entry_name false None e "" in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let EntryName (t, g) = interp_entry_name false TgAny e "" in + GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s)) | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" -> - let EntryName (t, g) = interp_entry_name false None e sep in - GramNonTerminal (!@loc, t, g, Some (Names.Id.of_string s)) + let EntryName (t, g) = interp_entry_name false TgAny e sep in + GramNonTerminal (!@loc, Genarg.unquote t, g, Some (Names.Id.of_string s)) | s = STRING -> GramTerminal s ] ] |