From d5dcb490f4f08dc1f5ae4158a26d264e03f808cc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 19 Aug 2019 04:02:09 +0200
Subject: [parsing] Remove extend AST in favor of gramlib constructors

We remove Coq's wrapper over gramlib's grammar constructors.
---
 coqpp/coqpp_main.ml                |   2 +-
 gramlib/grammar.ml                 | 102 ++++++++++++--
 gramlib/grammar.mli                |  21 ++-
 parsing/pcoq.ml                    | 264 ++++++-------------------------------
 parsing/pcoq.mli                   |  40 ++----
 plugins/ltac/tacentries.ml         |   8 +-
 user-contrib/Ltac2/g_ltac2.mlg     |   2 +-
 user-contrib/Ltac2/tac2core.ml     |   2 +-
 user-contrib/Ltac2/tac2entries.ml  |   6 +-
 user-contrib/Ltac2/tac2entries.mli |   2 +-
 vernac/egramcoq.ml                 |  14 +-
 vernac/egramml.ml                  |   8 +-
 vernac/egramml.mli                 |   4 +-
 vernac/pvernac.ml                  |   2 +-
 vernac/vernacextend.ml             |   6 +-
 vernac/vernacextend.mli            |   2 +-
 16 files changed, 182 insertions(+), 303 deletions(-)

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 70e400c29b..17f81c555c 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -266,7 +266,7 @@ let print_rule fmt r =
 let print_entry fmt e =
   let print_position_opt fmt pos = print_opt fmt print_position pos in
   let print_rules fmt rules = print_list fmt print_rule rules in
-  fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[(%a, %a)@]@]@ in@ "
+  fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[{ Pcoq.G.pos=%a; data=%a}@]@]@ in@ "
     e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
 
 let print_ast fmt ext =
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 818608674e..0eed42f290 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -80,12 +80,21 @@ module type S = sig
   module Unsafe : sig
     val clear_entry : 'a Entry.t -> unit
   end
-  val safe_extend : warning:(string -> unit) option ->
-    'a Entry.t -> Gramext.position option ->
-    (string option * Gramext.g_assoc option * 'a Production.t list)
-      list ->
-    unit
-  val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit
+
+  type 'a single_extend_statement =
+    string option * Gramext.g_assoc option * 'a Production.t list
+
+  type 'a extend_statement =
+    { pos : Gramext.position option
+    ; data : 'a single_extend_statement list
+    }
+
+  val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit
+  val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit
+
+  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+
+  val mk_rule : 'a pattern list -> string Rules.t
 
   (* Used in custom entries, should tweak? *)
   val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option
@@ -1659,13 +1668,18 @@ module Unsafe = struct
 
 end
 
-let safe_extend ~warning (e : 'a Entry.t) pos
-    (r :
-       (string option * Gramext.g_assoc option * 'a ty_production list)
-         list) =
-  extend_entry ~warning e pos r
+type 'a single_extend_statement =
+  string option * Gramext.g_assoc option * 'a ty_production list
+
+type 'a extend_statement =
+  { pos : Gramext.position option
+  ; data : 'a single_extend_statement list
+  }
+
+let safe_extend ~warning (e : 'a Entry.t) { pos; data } =
+  extend_entry ~warning e pos data
 
-let safe_delete_rule e r =
+let safe_delete_rule e (TProd (r,_act)) =
   let AnyS (symbols, _) = get_symbols r in
   delete_rule e symbols
 
@@ -1673,4 +1687,68 @@ let level_of_nonterm sym = match sym with
   | Snterml (_,l) -> Some l
   | _ -> None
 
+exception SelfSymbol
+
+let rec generalize_symbol :
+  type a tr s. (s, tr, a) Symbol.t -> (s, norec, a) ty_symbol =
+  function
+  | Stoken tok ->
+    Stoken tok
+  | Slist1 e ->
+    Slist1 (generalize_symbol e)
+  | Slist1sep (e, sep, b) ->
+    let e = generalize_symbol e in
+    let sep = generalize_symbol sep in
+    Slist1sep (e, sep, b)
+  | Slist0 e ->
+    Slist0 (generalize_symbol e)
+  | Slist0sep (e, sep, b) ->
+    let e = generalize_symbol e in
+    let sep = generalize_symbol sep in
+    Slist0sep (e, sep, b)
+  | Sopt e ->
+    Sopt (generalize_symbol e)
+  | Sself ->
+    raise SelfSymbol
+  | Snext ->
+    raise SelfSymbol
+  | Snterm e ->
+    Snterm e
+  | Snterml (e, l) ->
+    Snterml (e, l)
+  | Stree r ->
+    Stree (generalize_tree r)
+and generalize_tree : type a tr s .
+  (s, tr, a) ty_tree -> (s, norec, a) ty_tree = fun r ->
+  match r with
+  | Node (fi, n) ->
+    let fi = match fi with
+      | NoRec3 -> NoRec3
+      | MayRec3 -> raise SelfSymbol
+    in
+    let n = match n with
+      | { node; son; brother } ->
+        let node = generalize_symbol node in
+        let son = generalize_tree son in
+        let brother = generalize_tree brother in
+        { node; son; brother }
+    in
+    Node (fi, n)
+  | LocAct _ as r -> r
+  | DeadEnd as r -> r
+
+let generalize_symbol s =
+  try Some (generalize_symbol s)
+  with SelfSymbol -> None
+
+let rec mk_rule tok =
+  match tok with
+  | [] ->
+    let stop_e = Rule.stop in
+    TRules (stop_e, fun _ -> (* dropped anyway: *) "")
+  | tkn :: rem ->
+    let TRules (r, f) = mk_rule rem in
+    let r = Rule.next_norec r (Symbol.token tkn) in
+    TRules (r, fun _ -> f)
+
 end
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 4ac85bd358..4280181109 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -90,16 +90,23 @@ module type S = sig
     val clear_entry : 'a Entry.t -> unit
   end
 
-  val safe_extend : warning:(string -> unit) option ->
-    'a Entry.t -> Gramext.position option ->
-    (string option * Gramext.g_assoc option * 'a Production.t list)
-      list ->
-    unit
-  val safe_delete_rule : 'a Entry.t -> ('a, _, 'f, 'r) Rule.t -> unit
+  type 'a single_extend_statement =
+    string option * Gramext.g_assoc option * 'a Production.t list
+
+  type 'a extend_statement =
+    { pos : Gramext.position option
+    ; data : 'a single_extend_statement list
+    }
+
+  val safe_extend : warning:(string -> unit) option -> 'a Entry.t -> 'a extend_statement -> unit
+  val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit
+
+  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+
+  val mk_rule : 'a pattern list -> string Rules.t
 
   (* Used in custom entries, should tweak? *)
   val level_of_nonterm : ('a, norec, 'c) Symbol.t -> string option
-
 end
 (** Signature type of the functor [Grammar.GMake]. The types and
     functions are almost the same than in generic interface, but:
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8f7d6d1966..e10e4bb8dd 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -10,7 +10,6 @@
 
 open CErrors
 open Util
-open Extend
 open Genarg
 open Gramlib
 
@@ -19,47 +18,16 @@ open Gramlib
 type norec = Gramlib.Grammar.norec
 type mayrec = Gramlib.Grammar.mayrec
 
-type ('self, 'trec, 'a) symbol =
-| Atoken : 'c Tok.p -> ('self, norec, 'c) symbol
-| Alist1 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol
-| Alist1sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol
-              -> ('self, 'trec, 'a list) symbol
-| Alist0 : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a list) symbol
-| Alist0sep : ('self, 'trec, 'a) symbol * ('self, norec, _) symbol
-              -> ('self, 'trec, 'a list) symbol
-| Aopt : ('self, 'trec, 'a) symbol -> ('self, 'trec, 'a option) symbol
-| Aself : ('self, mayrec, 'self) symbol
-| Anext : ('self, mayrec, 'self) symbol
-| Aentry : 'a entry -> ('self, norec, 'a) symbol
-| Aentryl : 'a entry * string -> ('self, norec, 'a) symbol
-| Arules : 'a rules list -> ('self, norec, 'a) symbol
-
-and ('self, 'trec, _, 'r) rule =
-| Stop : ('self, norec, 'r, 'r) rule
-| Next : ('self, _, 'a, 'r) rule * ('self, _, 'b) symbol -> ('self, mayrec, 'b -> 'a, 'r) rule
-| NextNoRec : ('self, norec, 'a, 'r) rule * ('self, norec, 'b) symbol -> ('self, norec, 'b -> 'a, 'r) rule
-
-and 'a rules =
-| Rules : (_, norec, 'act, Loc.t -> 'a) rule * 'act -> 'a rules
-
-type 'a production_rule =
-| Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
-
 module G : sig
 
   include Grammar.S
     with type te = Tok.t
      and type 'c pattern = 'c Tok.p
-     and type 'a pattern = 'a Tok.p
-     and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol
-     and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule
-     and type 'a Rules.t = 'a rules
-     and type 'a Production.t = 'a production_rule
 
   val comment_state : Parsable.t -> ((int * int) * string) list
   val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option
-  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option
-  val mk_rule : 'a Tok.p list -> string rules
+  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+  val mk_rule : 'a Tok.p list -> string Rules.t
 
 end with type 'a Entry.t = 'a Extend.entry = struct
 
@@ -88,6 +56,12 @@ end with type 'a Entry.t = 'a Extend.entry = struct
 
   let tokens = G_.tokens
 
+  type 'a single_extend_statement = 'a G_.single_extend_statement
+  type 'a extend_statement = 'a G_.extend_statement =
+    { pos : Gramlib.Gramext.position option
+    ; data : 'a single_extend_statement list
+    }
+
   module Entry = struct
     include G_.Entry
 
@@ -105,164 +79,17 @@ end with type 'a Entry.t = 'a Extend.entry = struct
 
   end
 
-  module Symbol = struct
-    type ('self, 'trec, 'a) t = ('self, 'trec, 'a) symbol
-    let token tok = Atoken tok
-    let list0 e = Alist0 e
-    let list0sep e s _ = Alist0sep (e,s)
-    let list1 e = Alist1 e
-    let list1sep e s _ = Alist1sep (e,s)
-    let opt e = Aopt e
-    let self = Aself
-    let next = Anext
-    let nterm e = Aentry e
-    let nterml e s = Aentryl (e,s)
-    let rules ~warning:_ r = Arules r
-  end
-
-  module Rule = struct
-    type ('self, 'trec, 'f, 'r) t = ('self, 'trec, 'f, 'r) rule
-    let stop = Stop
-    let next a b = Next (a,b)
-    let next_norec a b = NextNoRec (a,b)
-  end
-
-  module Rules = struct
-    type 'a t = 'a rules
-    let make a f = Rules(a,f)
-  end
-
-  module Production = struct
-    type 'a t = 'a production_rule
-    let make a f = Rule(a,f)
-  end
-
-  module Unsafe = struct
-    let clear_entry = G_.Unsafe.clear_entry
-  end
-
-  (** FIXME: This is a hack around a deficient camlp5 API *)
-  type 'a any_production = AnyProduction : ('a, 'tr, 'f, Loc.t -> 'a) G_.Rule.t * 'f -> 'a any_production
-
-  let rec symbol_of_prod_entry_key : type s tr a. (s, tr, a) symbol -> (s, tr, a) G_.Symbol.t =
-    function
-    | Atoken t -> G_.Symbol.token t
-    | Alist1 s ->
-      let s = symbol_of_prod_entry_key s in
-      G_.Symbol.list1 s
-    | Alist1sep (s,sep) ->
-      let s = symbol_of_prod_entry_key s in
-      let sep = symbol_of_prod_entry_key sep in
-      G_.Symbol.list1sep s sep false
-    | Alist0 s ->
-      let s = symbol_of_prod_entry_key s in
-      G_.Symbol.list0 s
-    | Alist0sep (s,sep) ->
-      let s = symbol_of_prod_entry_key s in
-      let sep = symbol_of_prod_entry_key sep in
-      G_.Symbol.list0sep s sep false
-    | Aopt s ->
-      let s = symbol_of_prod_entry_key s in
-      G_.Symbol.opt s
-    | Aself -> G_.Symbol.self
-    | Anext -> G_.Symbol.next
-    | Aentry e -> G_.Symbol.nterm e
-    | Aentryl (e, n) -> G_.Symbol.nterml e n
-    | Arules rs ->
-      let warning msg = Feedback.msg_warning Pp.(str msg) in
-      G_.Symbol.rules ~warning:(Some warning) (List.map symbol_of_rules rs)
-
-  and symbol_of_rule : type s tr a r. (s, tr, a, r) rule -> (s, tr, a, r) G_.Rule.t = function
-    | Stop ->
-      G_.Rule.stop
-    | Next (r, s) ->
-      let r = symbol_of_rule r in
-      let s = symbol_of_prod_entry_key s in
-      G_.Rule.next r s
-    | NextNoRec (r, s) ->
-      let r = symbol_of_rule r in
-      let s = symbol_of_prod_entry_key s in
-      G_.Rule.next_norec r s
-
-  and symbol_of_rules : type a. a rules -> a G_.Rules.t = function
-    | Rules (r, act) ->
-      let symb = symbol_of_rule r in
-      G_.Rules.make symb act
-
-  let of_coq_production_rule : type a. a production_rule -> a any_production = function
-    | Rule (toks, act) ->
-      AnyProduction (symbol_of_rule toks, act)
-
-  let of_coq_single_extend_statement (lvl, assoc, rule) =
-    (lvl, assoc, List.map of_coq_production_rule rule)
-
-  let of_coq_extend_statement (pos, st) =
-    (pos, List.map of_coq_single_extend_statement st)
-
-  let fix_extend_statement (pos, st) =
-    let fix_single_extend_statement (lvl, assoc, rules) =
-      let fix_production_rule (AnyProduction (s, act)) = G_.Production.make s act in
-      (lvl, assoc, List.map fix_production_rule rules)
-    in
-    (pos, List.map fix_single_extend_statement st)
-
-  let safe_extend ~warning e pos ext =
-    let pos, ext = of_coq_extend_statement (pos,ext) in
-    let pos, ext = fix_extend_statement (pos, ext) in
-    G_.safe_extend ~warning e pos ext
-
-  let safe_delete_rule e r =
-    let r = symbol_of_rule r in
-    G_.safe_delete_rule e r
-
-  let level_of_nonterm = function
-    | Aentryl (_,l) -> Some l
-    | _ -> None
-
-  exception SelfSymbol
-  let rec generalize_symbol :
-    type a tr s. (s, tr, a) symbol -> (s, norec, a) 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
-      Alist1sep (e, sep)
-    | Alist0 e ->
-      Alist0 (generalize_symbol e)
-    | Alist0sep (e, sep) ->
-      let e = generalize_symbol e in
-      let sep = generalize_symbol sep in
-      Alist0sep (e, sep)
-    | Aopt e ->
-      Aopt (generalize_symbol e)
-    | Aself ->
-      raise SelfSymbol
-    | Anext ->
-      raise SelfSymbol
-    | Aentry e ->
-      Aentry e
-    | Aentryl (e, l) ->
-      Aentryl (e, l)
-    | Arules r ->
-      Arules r
-
-  let generalize_symbol s =
-    try Some (generalize_symbol s)
-    with SelfSymbol -> None
-
-  let rec mk_rule tok =
-    match tok with
-    | [] ->
-      let stop_e = Stop in
-      Rules (stop_e, fun _ -> (* dropped anyway: *) "")
-    | tkn :: rem ->
-      let Rules (r, f) = mk_rule rem in
-      let r = Rule.next_norec r (Symbol.token tkn) in
-      Rules (r, fun _ -> f)
+  module Symbol = G_.Symbol
+  module Rule = G_.Rule
+  module Rules = G_.Rules
+  module Production = G_.Production
+  module Unsafe = G_.Unsafe
+
+  let safe_extend = G_.safe_extend
+  let safe_delete_rule = G_.safe_delete_rule
+  let level_of_nonterm = G_.level_of_nonterm
+  let generalize_symbol = G_.generalize_symbol
+  let mk_rule = G_.mk_rule
 end
 
 module Parsable = struct
@@ -349,21 +176,9 @@ end
 (** Type of reinitialization data *)
 type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
 
-type 'a single_extend_statement =
-  string option *
-  (* Level *)
-  Gramlib.Gramext.g_assoc option *
-  (* Associativity *)
-  'a production_rule list
-  (* Symbol list with the interpretation function *)
-
-type 'a extend_statement =
-  Gramlib.Gramext.position option *
-  'a single_extend_statement list
-
 type extend_rule =
-| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
-| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
+| ExtendRule : 'a G.Entry.t * 'a G.extend_statement -> extend_rule
+| ExtendRuleReinit : 'a G.Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule
 
 module EntryCommand = Dyn.Make ()
 module EntryData = struct type _ t = Ex : 'b G.Entry.t String.Map.t -> ('a * 'b) t end
@@ -382,39 +197,38 @@ let camlp5_entries = ref EntryDataMap.empty
 
 (** Deletion *)
 
-let grammar_delete e (pos,rls) =
+let grammar_delete e { G.pos; data } =
   List.iter
     (fun (n,ass,lev) ->
-      List.iter (fun (Rule(pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
-    (List.rev rls)
+      List.iter (fun pil -> G.safe_delete_rule e pil) (List.rev lev))
+    (List.rev data)
 
-let grammar_delete_reinit e reinit (pos, rls) =
-  grammar_delete e (pos, rls);
+let grammar_delete_reinit e reinit ({ G.pos; data } as d)=
+  grammar_delete e d;
   let a, ext = reinit in
   let lev = match pos with
     | Some (Gramext.Level n) -> n
     | _ -> assert false
   in
   let warning msg = Feedback.msg_warning Pp.(str msg) in
-  (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
+  let ext = { G.pos = Some ext; data = [Some lev,Some a,[]] } in
+  G.safe_extend ~warning:(Some warning) e ext
 
 (** Extension *)
 
-let grammar_extend e (pos,ext) =
-  let undo () = grammar_delete e (pos,ext) in
-  let redo () = G.safe_extend ~warning:None e pos ext in
+let grammar_extend e ext =
+  let undo () = grammar_delete e ext in
+  let redo () = G.safe_extend ~warning:None e ext in
   camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
   redo ()
 
 let grammar_extend_sync e ext =
   camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state;
-  let pos, ext = ext in
-  G.safe_extend ~warning:None e pos ext
+  G.safe_extend ~warning:None e ext
 
 let grammar_extend_sync_reinit e reinit ext =
   camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
-  let pos, ext = ext in
-  G.safe_extend ~warning:None e pos ext
+  G.safe_extend ~warning:None e ext
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -467,7 +281,8 @@ let eoi_entry en =
   let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in
   let act = fun _ x loc -> x in
   let warning msg = Feedback.msg_warning Pp.(str msg) in
-  Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.Production.make symbs act]);
+  let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
+  Gram.safe_extend ~warning:(Some warning) e ext;
   e
 
 let map_entry f en =
@@ -475,7 +290,8 @@ let map_entry f en =
   let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in
   let act = fun x loc -> f x in
   let warning msg = Feedback.msg_warning Pp.(str msg) in
-  Gram.safe_extend ~warning:(Some warning) e None (make_rule [G.Production.make symbs act]);
+  let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
+  Gram.safe_extend ~warning:(Some warning) e ext;
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -620,12 +436,12 @@ module Module =
     let module_type = Entry.create "module_type"
   end
 
-let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) =
+let epsilon_value (type s tr a) f (e : (s, tr, a) G.Symbol.t) =
   let r = G.Production.make (G.Rule.next G.Rule.stop e) (fun x _ -> f x) in
-  let ext = [None, None, [r]] in
   let entry = G.Entry.make "epsilon" in
   let warning msg = Feedback.msg_warning Pp.(str msg) in
-  let () = G.safe_extend ~warning:(Some warning) entry None ext in
+  let ext = { G.pos = None; data = [None, None, [r]] } in
+  let () = G.safe_extend ~warning:(Some warning) entry ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e7e3e9442b..f83109d39a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -223,51 +223,26 @@ module Module :
 
 (** {5 Type-safe grammar extension} *)
 
-type ('self, 'trec, 'a) symbol
-type ('self, 'trec, _, 'r) rule
-
 type norec = Gramlib.Grammar.norec
 type mayrec = Gramlib.Grammar.mayrec
 
-type 'a rules
-type 'a production_rule
-
 module G : sig
 
   include Gramlib.Grammar.S
 
   val level_of_nonterm : ('a,norec,'c) Symbol.t -> string option
-  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) symbol option
-  val mk_rule : 'a Tok.p list -> string rules
+  val generalize_symbol : ('a, 'tr, 'c) Symbol.t -> ('a, norec, 'c) Symbol.t option
+  val mk_rule : 'a Tok.p list -> string Rules.t
 
 end with type 'a Entry.t = 'a Entry.t
      and type te = Tok.t
      and type 'a pattern = 'a Tok.p
-     and type ('self, 'trec, 'a) Symbol.t = ('self, 'trec, 'a) symbol
-     and type ('self, 'trec, 'f, 'r) Rule.t = ('self, 'trec, 'f, 'r) rule
-     and type 'a Rules.t = 'a rules
-     and type 'a Production.t = 'a production_rule
 
-val epsilon_value : ('a -> 'self) -> ('self, _, 'a) symbol -> 'self option
+val epsilon_value : ('a -> 'self) -> ('self, _, 'a) G.Symbol.t -> 'self option
 
 (** {5 Extending the parser without synchronization} *)
 
-type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
-(** Type of reinitialization data *)
-
-type 'a single_extend_statement =
-  string option *
-  (* Level *)
-  Gramlib.Gramext.g_assoc option *
-  (* Associativity *)
-  'a production_rule list
-  (* Symbol list with the interpretation function *)
-
-type 'a extend_statement =
-  Gramlib.Gramext.position option *
-  'a single_extend_statement list
-
-val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit
+val grammar_extend : 'a Entry.t -> 'a G.extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)
@@ -283,9 +258,12 @@ type 'a grammar_command
 (** Type of synchronized parsing extensions. The ['a] type should be
     marshallable. *)
 
+type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
+(** Type of reinitialization data *)
+
 type extend_rule =
-| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
-| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a G.extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a G.extend_statement -> extend_rule
 
 type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 (** Grammar extension entry point. Given some ['a] and a current grammar state,
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 6b83590b1d..eed7f07b2e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -48,7 +48,7 @@ let atactic n =
   else Pcoq.G.Symbol.nterml Pltac.tactic_expr (string_of_int n)
 
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.symbol -> entry_name
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.G.Symbol.t -> entry_name
 
 (** Quite ad-hoc *)
 let get_tacentry n m =
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
-  let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in
+  let r = ExtendRule (entry, { G.pos; data=[(None, None, [rules])]}) in
   ([r], state)
 
 let tactic_grammar =
@@ -421,7 +421,7 @@ let create_ltac_quotation name cast (e, l) =
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
   let gram = (level, assoc, [Pcoq.G.Production.make rule action]) in
-  Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
+  Pcoq.grammar_extend Pltac.tactic_arg {G.pos=None; data=[gram]}
 
 (** Command *)
 
@@ -765,7 +765,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
     e
   | Vernacextend.Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
-    let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
+    let () = Pcoq.grammar_extend e {G.pos=None; data=[(None, None, rules)]} in
     e
   in
   let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 8b3203c8dd..477672ebdb 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -861,7 +861,7 @@ let rules = [
 ] in
 
 Hook.set Tac2entries.register_constr_quotations begin fun () ->
-  Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
+  Pcoq.grammar_extend Pcoq.Constr.operconstr {G.pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
 end
 
 }
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 547ca0c2ed..0946c88228 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1590,7 +1590,7 @@ 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 : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Pcoq.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule
 
 let rec make_seq_rule = function
 | [] ->
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index c5f081eab9..7c4971db8c 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -558,7 +558,7 @@ type 'a token =
 | TacNonTerm of Name.t * 'a
 
 type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
 
 type scope_interpretation = sexpr list -> scope_rule
 
@@ -611,7 +611,7 @@ type synext = {
 
 type krule =
 | KRule :
-  (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.rule *
+  (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.G.Rule.t *
   ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
 
 let rec get_rule (tok : scope_rule token list) : krule = match tok with
@@ -643,7 +643,7 @@ let perform_notation syn st =
   | Some lev -> Some (string_of_int lev)
   in
   let rule = (lev, None, [rule]) in
-  ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st)
+  ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.G.pos=None; data=[rule]})], st)
 
 let ltac2_notation =
   Pcoq.create_grammar_command "ltac2-notation" perform_notation
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index 4938e96cae..1efac697aa 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit
 (** {5 Notations} *)
 
 type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.G.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
 
 type scope_interpretation = sexpr list -> scope_rule
 
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 43029f4d53..88bcf1d477 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -332,8 +332,8 @@ let make_sep_rules = function
     Pcoq.G.Symbol.rules ~warning:None [r]
 
 type ('s, 'a) mayrec_symbol =
-| MayRecNo : ('s, norec, 'a) symbol -> ('s, 'a) mayrec_symbol
-| MayRecMay : ('s, mayrec, 'a) symbol -> ('s, 'a) mayrec_symbol
+| MayRecNo : ('s, norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
 
 let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_symbol = fun custom p assoc from forpat ->
   if is_binder_level custom from p
@@ -458,8 +458,8 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env ->
     ty_eval rem f { env with constrs; constrlists; }
 
 type ('s, 'a, 'r) mayrec_rule =
-| MayRecRNo : ('s, norec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule
-| MayRecRMay : ('s, mayrec, 'a, 'r) rule -> ('s, 'a, 'r) mayrec_rule
+| MayRecRNo : ('s, norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
 
 let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) mayrec_rule = function
 | TyStop -> MayRecRNo G.Rule.stop
@@ -501,7 +501,7 @@ let target_to_bool : type r. r target -> bool = function
 | ForPattern -> true
 
 let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
-  let empty = (pos, [(name, p4assoc, [])]) in
+  let empty = { G.pos; data = [(name, p4assoc, [])] } in
   match reinit with
   | None ->
     ExtendRule (target_entry where forpat, empty)
@@ -562,9 +562,9 @@ let extend_constr state forpat ng =
       name, p4assoc, [r] in
     let r = match reinit with
       | None ->
-        ExtendRule (entry, (pos, [rule]))
+        ExtendRule (entry, { G.pos; data = [rule]})
       | Some reinit ->
-        ExtendRuleReinit (entry, reinit, (pos, [rule]))
+        ExtendRuleReinit (entry, reinit, { G.pos; data = [rule]})
     in
     (accu @ empty_rules @ [r], state)
   in
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 175217803f..00a239f56e 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,13 +19,13 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      ('a raw_abstract_argument_type * ('s, _, 'a) symbol) Loc.located -> 's grammar_prod_item
+      ('a raw_abstract_argument_type * ('s, _, 'a) G.Symbol.t) Loc.located -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
 type ('self, 'tr, _, 'r) ty_rule =
 | TyStop : ('self, Pcoq.norec, 'r, 'r) ty_rule
-| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.symbol * 'b ty_arg option ->
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Pcoq.G.Symbol.t * 'b ty_arg option ->
   ('self, Pcoq.mayrec, 'b -> 'a, 'r) ty_rule
 
 type ('self, 'r) any_ty_rule =
@@ -44,7 +44,7 @@ let rec ty_rule_of_gram = function
   let r = TyNext (rem, tok, inj) in
   AnyTyRule r
 
-let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.rule = function
+let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.G.Rule.t = function
 | TyStop -> Pcoq.G.Rule.stop
 | TyNext (rem, tok, _) -> Pcoq.G.Rule.next (ty_erase rem) tok
 
@@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl =
   vernac_exts := (s,gl) :: !vernac_exts;
   let mkact loc l = VernacExtend (s, l) in
   let rules = [make_rule mkact gl] in
-  grammar_extend nt (None, [None, None, rules])
+  grammar_extend nt { G.pos=None; data=[None, None, rules]}
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index e6e4748b59..77198452b9 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -18,7 +18,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
-      ('s, _, 'a) Pcoq.symbol) Loc.located -> 's grammar_prod_item
+      ('s, _, 'a) Pcoq.G.Symbol.t) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
   extend_name -> vernac_expr Pcoq.Entry.t option ->
@@ -32,4 +32,4 @@ val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.gena
 
 val make_rule :
   (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
-  'a grammar_prod_item list -> 'a Pcoq.production_rule
+  'a grammar_prod_item list -> 'a Pcoq.G.Production.t
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 27b8a5bda2..9a9c96064d 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -57,7 +57,7 @@ module Vernac_ =
         Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi);
         Pcoq.G.(Production.make (Rule.next Rule.stop (Symbol.nterm vernac_control)) act_vernac);
       ] in
-      Pcoq.grammar_extend main_entry (None, [None, None, rule])
+      Pcoq.(grammar_extend main_entry {G.pos=None; data=[None, None, rule]})
 
     let select_tactic_entry spec =
       match spec with
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index fc6ece27cd..ac4d33c926 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -166,7 +166,7 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_c
     | Some Refl -> untype_command ty (f v) args
   end
 
-let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Pcoq.norec, a) Pcoq.symbol =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Pcoq.norec, a) Pcoq.G.Symbol.t =
   let open Extend in function
 | TUlist1 l -> Pcoq.G.Symbol.list1 (untype_user_symbol l)
 | TUlist1sep (l, s) -> Pcoq.G.Symbol.list1sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
@@ -229,7 +229,7 @@ let vernac_extend ~command ?classifier ?entry ext =
 
 type 'a argument_rule =
 | Arg_alias of 'a Pcoq.Entry.t
-| Arg_rules of 'a Pcoq.production_rule list
+| Arg_rules of 'a Pcoq.G.Production.t list
 
 type 'a vernac_argument = {
   arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
@@ -244,7 +244,7 @@ let vernac_argument_extend ~name arg =
     e
   | Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
-    let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
+    let () = Pcoq.grammar_extend e {Pcoq.G.pos=None; data=[(None, None, rules)]} in
     e
   in
   let pr = arg.arg_printer in
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 0acb5f43f9..4d9537b6ff 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -111,7 +111,7 @@ type 'a argument_rule =
 | Arg_alias of 'a Pcoq.Entry.t
   (** This is used because CAMLP5 parser can be dumb about rule factorization,
       which sometimes requires two entries to be the same. *)
-| Arg_rules of 'a Pcoq.production_rule list
+| Arg_rules of 'a Pcoq.G.Production.t list
   (** There is a discrepancy here as we use directly extension rules and thus
     entries instead of ty_user_symbol and thus arguments as roots. *)
 
-- 
cgit v1.2.3