[parsing] Split Tok.t into Tok.t and Tok.pattern

Tokens were having a double role:
- the output of the lexer
- the items of grammar entries, especially terminals

Now tokens are the output of the lexer, and this paves the way for
using a richer data type, eg including Loc.t

Patterns, as in Plexing.pattern, only represent patterns (for tokens)
and now have a bit more structure (eg the wildcard is represented
as None, not as "", while a regular pattern for "x" as Some "x")

1 files changed, 4 insertions, 5 deletions

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3da12e7714..781fd404f8 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -23,7 +23,6 @@ open Libobject
 open Constrintern
 open Vernacexpr
 open Libnames
-open Tok
 open Notation
 open Nameops
 
@@ -575,20 +574,20 @@ let is_not_small_constr = function
   | _ -> false
 
 let rec define_keywords_aux = function
-  | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
+  | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",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(KEYWORD k) :: define_keywords_aux l
+      n1 :: GramConstrTerminal(Tok.pattern_for_KEYWORD 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 k)::l ->
+  | GramConstrTerminal("IDENT", Some k)::l ->
       Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword");
       CLexer.add_keyword k;
-      GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
+      GramConstrTerminal(Tok.pattern_for_KEYWORD k) :: define_keywords_aux l
   | l -> define_keywords_aux l
 
 let distribute a ll = List.map (fun l -> a @ l) ll