diff options
| author | Pierre Roux | 2019-02-17 10:10:22 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-03-31 23:17:55 +0200 |
| commit | eadb00648127c9a535b533d51189dce41ef16db7 (patch) | |
| tree | 1e5db53e73950ca4c7d7d9ae5e01a5d5c83ac32f /vernac/metasyntax.ml | |
| parent | 5dd3c18f4e50eef53ae4413b7b80951f17edad5f (diff) | |
Multiple payload types in tokens
Instead of just string (and empty strings for tokens without payload)
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 781fd404f8..b5e9e1b0d5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -574,20 +574,20 @@ let is_not_small_constr = function | _ -> false let rec define_keywords_aux = function - | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",Some k) :: l + | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(Tok.PIDENT (Some k)) :: l when is_not_small_constr e -> Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; - n1 :: GramConstrTerminal(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l + n1 :: GramConstrTerminal(Tok.PKEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l | [] -> [] (* Ensure that IDENT articulation terminal symbols are keywords *) let define_keywords = function - | GramConstrTerminal("IDENT", Some k)::l -> + | GramConstrTerminal(Tok.PIDENT (Some k))::l -> Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; - GramConstrTerminal(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l + GramConstrTerminal(Tok.PKEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l let distribute a ll = List.map (fun l -> a @ l) ll |