Merge pull request coq/ltac2#114 from proux01/token-type

[coq] Adapt to coq/coq#9815

4 files changed, 22 insertions, 32 deletions

diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg
index 2483ef459a..fcf5d59ec9 100644
--- a/src/g_ltac2.mlg
+++ b/src/g_ltac2.mlg
@@ -831,7 +831,7 @@ let open Tok in
 let (++) r s = Next (r, s) in
 let rules = [
   Rule (
-    Stop ++ Aentry test_dollar_ident ++ Atoken (pattern_for_KEYWORD "$") ++ Aentry Prim.ident,
+    Stop ++ Aentry test_dollar_ident ++ Atoken (PKEYWORD "$") ++ Aentry Prim.ident,
     begin fun id _ _ loc ->
       let id = Loc.tag ~loc id in
       let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
@@ -840,7 +840,7 @@ let rules = [
   );
 
   Rule (
-    Stop ++ Aentry test_ampersand_ident ++ Atoken (pattern_for_KEYWORD "&") ++ Aentry Prim.ident,
+    Stop ++ Aentry test_ampersand_ident ++ Atoken (PKEYWORD "&") ++ Aentry Prim.ident,
     begin fun id _ _ loc ->
       let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
       let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
@@ -849,8 +849,8 @@ let rules = [
   );
 
   Rule (
-    Stop ++ Atoken (pattern_for_IDENT "ltac2") ++ Atoken (pattern_for_KEYWORD ":") ++
-      Atoken (pattern_for_KEYWORD "(") ++ Aentry tac2expr ++ Atoken (pattern_for_KEYWORD ")"),
+    Stop ++ Atoken (PIDENT (Some "ltac2")) ++ Atoken (PKEYWORD ":") ++
+      Atoken (PKEYWORD "(") ++ Aentry tac2expr ++ Atoken (PKEYWORD ")"),
     begin fun _ tac _ _ _ loc ->
       let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
       CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 0f85f56c22..a584933e00 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1251,7 +1251,7 @@ open CAst
 
 let () = add_scope "keyword" begin function
 | [SexprStr {loc;v=s}] ->
-  let scope = Extend.Atoken (Tok.pattern_for_KEYWORD s) in
+  let scope = Extend.Atoken (Tok.PKEYWORD s) in
   Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
 | arg -> scope_fail "keyword" arg
 end
@@ -1381,34 +1381,25 @@ let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
 open Extend
 exception SelfSymbol
 
-type 'a any_symbol = { any_symbol : 'r. ('r, 'a) symbol }
-
 let rec generalize_symbol :
-  type a s. (s, a) Extend.symbol -> a any_symbol = function
-| Atoken tok ->
-  { any_symbol = Atoken tok }
-| Alist1 e ->
-  let e = generalize_symbol e in
-  { any_symbol = Alist1 e.any_symbol }
+  type a tr s. (s, tr, a) Extend.symbol -> (s, Extend.norec, a) Extend.symbol = function
+| Atoken tok -> Atoken tok
+| Alist1 e -> Alist1 (generalize_symbol e)
 | Alist1sep (e, sep) ->
   let e = generalize_symbol e in
   let sep = generalize_symbol sep in
-  { any_symbol = Alist1sep (e.any_symbol, sep.any_symbol) }
-| Alist0 e ->
-  let e = generalize_symbol e in
-  { any_symbol = Alist0 e.any_symbol }
+  Alist1sep (e, sep)
+| Alist0 e -> Alist0 (generalize_symbol e)
 | Alist0sep (e, sep) ->
   let e = generalize_symbol e in
   let sep = generalize_symbol sep in
-  { any_symbol = Alist0sep (e.any_symbol, sep.any_symbol) }
-| Aopt e ->
-  let e = generalize_symbol e in
-  { any_symbol = Aopt e.any_symbol }
+  Alist0sep (e, sep)
+| Aopt e -> Aopt (generalize_symbol e)
 | Aself -> raise SelfSymbol
 | Anext -> raise SelfSymbol
-| Aentry e -> { any_symbol = Aentry e }
-| Aentryl (e, l) -> { any_symbol = Aentryl (e, l) }
-| Arules r -> { any_symbol = Arules r }
+| Aentry e -> Aentry e
+| Aentryl (e, l) -> Aentryl (e, l)
+| Arules r -> Arules r
 
 type _ converter =
 | CvNil : (Loc.t -> raw_tacexpr) converter
@@ -1420,17 +1411,16 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function
 | CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu)
 
 type seqrule =
-| Seqrule : ('act, Loc.t -> raw_tacexpr) norec_rule * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Extend.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule
 
 let rec make_seq_rule = function
 | [] ->
-  let r = { norec_rule = Stop } in
-  Seqrule (r, CvNil)
+  Seqrule (Stop, CvNil)
 | tok :: rem ->
   let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in
   let scope = generalize_symbol scope in
   let Seqrule (r, c) = make_seq_rule rem in
-  let r = { norec_rule = Next (r.norec_rule, scope.any_symbol) } in
+  let r = NextNoRec (r, scope) in
   let f = match tok with
   | SexprStr _ -> None (* Leave out mere strings *)
   | _ -> Some f
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index bce58653e6..9fd01426de 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -514,7 +514,7 @@ type 'a token =
 | TacNonTerm of Name.t * 'a
 
 type scope_rule =
-| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
 
 type scope_interpretation = sexpr list -> scope_rule
 
@@ -539,7 +539,7 @@ let parse_scope = function
     CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id)
 | SexprStr {v=str} ->
   let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in
-  ScopeRule (Extend.Atoken (Tok.pattern_for_IDENT str), (fun _ -> v_unit))
+  ScopeRule (Extend.Atoken (Tok.PIDENT (Some str)), (fun _ -> v_unit))
 | tok ->
   let loc = loc_of_token tok in
   CErrors.user_err ?loc (str "Invalid parsing token")
@@ -567,7 +567,7 @@ type synext = {
 
 type krule =
 | KRule :
-  (raw_tacexpr, 'act, Loc.t -> raw_tacexpr) Extend.rule *
+  (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Extend.rule *
   ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
 
 let rec get_rule (tok : scope_rule token list) : krule = match tok with
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 28b2120537..d493192bb3 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -33,7 +33,7 @@ val register_notation : ?local:bool -> sexpr list -> int option ->
 (** {5 Notations} *)
 
 type scope_rule =
-| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
 
 type scope_interpretation = sexpr list -> scope_rule