Merge PR #9733: [lexer] keyword protected quotation token for arbitrary text

Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot

3 files changed, 9 insertions, 10 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 1a07d74a0e..f96b567f1b 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -247,10 +247,10 @@ type (_, _) entry =
 | TTReference : ('self, qualid) entry
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
 | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
-| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
+| TTConstrList : prod_info * Tok.pattern list * 'r target -> ('r, 'r list) entry
 | TTPattern : int -> ('self, cases_pattern_expr) entry
 | TTOpenBinderList : ('self, local_binder_expr list) entry
-| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry
+| TTClosedBinderList : Tok.pattern list -> ('self, local_binder_expr list list) entry
 
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
@@ -319,7 +319,7 @@ let is_binder_level from e = match e with
 let make_sep_rules = function
   | [tk] -> Atoken tk
   | tkl ->
-  let rec mkrule : Tok.t list -> string rules = function
+  let rec mkrule : Tok.pattern list -> string rules = function
   | [] -> Rules ({ norec_rule = Stop }, fun _ -> (* dropped anyway: *) "")
   | tkn :: rem ->
     let Rules ({ norec_rule = r }, f) = mkrule rem in
@@ -406,7 +406,7 @@ match e with
 | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
 
 type (_, _) ty_symbol =
-| TyTerm : Tok.t -> ('s, string) ty_symbol
+| TyTerm : Tok.pattern -> ('s, string) ty_symbol
 | TyNonTerm : 's target * ('s, 'a) entry * ('s, 'a) symbol * bool -> ('s, 'a) ty_symbol
 
 type ('self, _, 'r) ty_rule =
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
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 994fad85f0..9438b9749f 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -55,7 +55,7 @@ module Vernac_ =
       let act_vernac v loc = Some CAst.(make ~loc v) in
       let act_eoi _ loc = None in
       let rule = [
-        Rule (Next (Stop, Atoken Tok.EOI), act_eoi);
+        Rule (Next (Stop, Atoken Tok.pattern_for_EOI), act_eoi);
         Rule (Next (Stop, Aentry vernac_control), act_vernac);
       ] in
       Pcoq.grammar_extend main_entry None (None, [None, None, rule])