Merge PR #11647: [rfc] Consolidation of parsing interfaces

Ack-by: SkySkimmer
Reviewed-by: ppedrot

24 files changed, 460 insertions, 585 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 39c801197b..f2e0c362b4 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -103,6 +103,9 @@ before_script:
   interruptible: true
   dependencies: []
   script:
+    # flambda can be pretty stack hungry, specially with -O3
+    # See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244
+    - ulimit -s 16384
     - set -e
     - make -f Makefile.dune world
     - set +e
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index bdffabf0b2..43cd6f1784 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -115,7 +115,7 @@ let print_local fmt ext =
   match locals with
   | [] -> ()
   | e :: locals ->
-    let mk_e fmt e = fprintf fmt "Pcoq.Entry.create \"%s\"" e in
+    let mk_e fmt e = fprintf fmt "Pcoq.Entry.make \"%s\"" e in
     let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in
     let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in
     let () = List.iter iter locals in
@@ -217,43 +217,43 @@ let rec print_prod fmt p =
 
 and print_extrule fmt (tkn, vars, body) =
   let tkn = List.rev tkn in
-  fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" (print_symbols ~norec:false) tkn print_fun (vars, body)
+  fprintf fmt "@[Pcoq.Production.make@ @[(%a)@]@ @[(%a)@]@]" (print_symbols ~norec:false) tkn print_fun (vars, body)
 
 and print_symbols ~norec fmt = function
-| [] -> fprintf fmt "Extend.Stop"
+| [] -> fprintf fmt "Pcoq.Rule.stop"
 | tkn :: tkns ->
-  let c = if norec then "Extend.NextNoRec" else "Extend.Next" in
-  fprintf fmt "%s @[(%a,@ %a)@]" c (print_symbols ~norec) tkns print_symbol tkn
+  let c = if norec then "Pcoq.Rule.next_norec" else "Pcoq.Rule.next" in
+  fprintf fmt "%s @[(%a)@ (%a)@]" c (print_symbols ~norec) tkns print_symbol tkn
 
 and print_symbol fmt tkn = match tkn with
 | SymbToken (t, s) ->
-  fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s)
+  fprintf fmt "(Pcoq.Symbol.token (%a))" print_tok (t, s)
 | SymbEntry (e, None) ->
-  fprintf fmt "(Extend.Aentry %s)" e
+  fprintf fmt "(Pcoq.Symbol.nterm %s)" e
 | SymbEntry (e, Some l) ->
-  fprintf fmt "(Extend.Aentryl (%s, %a))" e print_string l
+  fprintf fmt "(Pcoq.Symbol.nterml %s (%a))" e print_string l
 | SymbSelf ->
-  fprintf fmt "Extend.Aself"
+  fprintf fmt "Pcoq.Symbol.self"
 | SymbNext ->
-  fprintf fmt "Extend.Anext"
+  fprintf fmt "Pcoq.Symbol.next"
 | SymbList0 (s, None) ->
-  fprintf fmt "(Extend.Alist0 %a)" print_symbol s
+  fprintf fmt "(Pcoq.Symbol.list0 %a)" print_symbol s
 | SymbList0 (s, Some sep) ->
-  fprintf fmt "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep
+  fprintf fmt "(Pcoq.Symbol.list0sep (%a) (%a) false)" print_symbol s print_symbol sep
 | SymbList1 (s, None) ->
-  fprintf fmt "(Extend.Alist1 %a)" print_symbol s
+  fprintf fmt "(Pcoq.Symbol.list1 (%a))" print_symbol s
 | SymbList1 (s, Some sep) ->
-  fprintf fmt "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep
+  fprintf fmt "(Pcoq.Symbol.list1sep (%a) (%a) false)" print_symbol s print_symbol sep
 | SymbOpt s ->
-  fprintf fmt "(Extend.Aopt %a)" print_symbol s
+  fprintf fmt "(Pcoq.Symbol.opt %a)" print_symbol s
 | SymbRules rules ->
   let pr fmt (r, body) =
     let (vars, tkn) = List.split r in
     let tkn = List.rev tkn in
-    fprintf fmt "Extend.Rules @[(%a,@ (%a))@]" (print_symbols ~norec:true) tkn print_fun (vars, body)
+    fprintf fmt "Pcoq.Rules.make @[(%a)@ (%a)@]" (print_symbols ~norec:true) tkn print_fun (vars, body)
   in
   let pr fmt rules = print_list fmt pr rules in
-  fprintf fmt "(Extend.Arules %a)" pr (List.rev rules)
+  fprintf fmt "(Pcoq.Symbol.rules %a)" pr (List.rev rules)
 | SymbQuote c ->
   fprintf fmt "(%s)" c
 
@@ -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.pos=%a; data=%a}@]@]@ in@ "
     e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
 
 let print_ast fmt ext =
@@ -452,7 +452,7 @@ let terminal s =
   let p =
     if s <> "" && s.[0] >= '0' && s.[0] <= '9' then "CLexer.terminal_numeral"
     else "CLexer.terminal" in
-  let c = Printf.sprintf "Extend.Atoken (%s \"%s\")" p s in
+  let c = Printf.sprintf "Pcoq.Symbol.token (%s \"%s\")" p s in
   SymbQuote c
 
 let rec parse_symb self = function
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 0024d70466..d6951fff6d 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -8,8 +8,6 @@ open Util
 
 (* Functorial interface *)
 
-module type GLexerType = Plexing.Lexer
-
 type norec
 type mayrec
 
@@ -20,6 +18,7 @@ module type S = sig
   module Parsable : sig
     type t
     val make : ?loc:Loc.t -> char Stream.t -> t
+    val comments : t -> ((int * int) * string) list
   end
 
   val tokens : string -> (string option * int) list
@@ -27,6 +26,7 @@ module type S = sig
   module Entry : sig
     type 'a t
     val make : string -> 'a t
+    val create : string -> 'a t
     val parse : 'a t -> Parsable.t -> 'a
     val name : 'a t -> string
     val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t
@@ -51,7 +51,7 @@ module type S = sig
     val self : ('self, mayrec, 'self) t
     val next : ('self, mayrec, 'self) t
     val token : 'c pattern -> ('self, norec, 'c) t
-    val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+    val rules : 'a Rules.t list -> ('self, norec, 'a) t
 
   end and Rule : sig
 
@@ -77,21 +77,39 @@ module type S = sig
     val make : ('a, _, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t
   end
 
-  module Unsafe :
-  sig
+  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 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
+
+module type ExtS = sig
+
+  include S
+
+  val safe_extend : 'a Entry.t -> 'a extend_statement -> unit
+  val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit
+
+  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
+
 end
 
 (* Implementation *)
 
-module GMake (L : GLexerType) = struct
+module GMake (L : Plexing.S) = struct
 
 type te = L.te
 type 'c pattern = 'c L.pattern
@@ -324,7 +342,7 @@ let and_and_tree (type s tr' trt tr trn trs trb f) (ar : (tr', trt, tr) ty_and_r
   | MayRec2, _, MayRec -> MayRec2 | MayRec2, _, NoRec -> MayRec2
   | NoRec2, NoRec3, NoRec -> NoRec2
 
-let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree =
+let insert_tree (type s trs trt tr p k a) entry_name (ar : (trs, trt, tr) ty_and_ex) (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, tr, a) ty_tree =
   let rec insert : type trs trt tr p f k. (trs, trt, tr) ty_and_ex -> (s, trs, p) ty_symbols -> (p, k, f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree  =
     fun ar symbols pf tree action ->
     match symbols, pf with
@@ -338,15 +356,15 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t
         | NR10, Node (_, n) -> Node (MayRec3, node n)
         | NR11, Node (NoRec3, n) -> Node (NoRec3, node n)
         | NR11, LocAct (old_action, action_list) ->
-          begin match warning with
-            | None -> ()
-            | Some warn_fn ->
+          (* What to do about this warning? For now it is disabled *)
+          if false then
+            begin
               let msg =
                 "<W> Grammar extension: " ^
                 (if entry_name = "" then "" else "in ["^entry_name^"%s], ") ^
                 "some rule has been masked" in
-              warn_fn msg
-          end;
+              Feedback.msg_warning (Pp.str msg)
+            end;
           LocAct (action, old_action :: action_list)
         | NR11, DeadEnd -> LocAct (action, [])
   and insert_in_tree : type trs trs' trs'' trt tr a p f k. (trs'', trt, tr) ty_and_ex -> (trs, trs', trs'') ty_and_rec -> (s, trs, a) ty_symbol -> (s, trs', p) ty_symbols -> (p, k, a -> f) rel_prod -> (s, trt, f) ty_tree -> k -> (s, tr, f) ty_tree =
@@ -405,14 +423,14 @@ let insert_tree (type s trs trt tr p k a) ~warning entry_name (ar : (trs, trt, t
   in
   insert ar gsymbols pf tree action
 
-let insert_tree_norec (type s p k a) ~warning entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, norec, a) ty_tree =
-  insert_tree ~warning entry_name NR11 gsymbols pf action tree
+let insert_tree_norec (type s p k a) entry_name (gsymbols : (s, norec, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, norec, a) ty_tree) : (s, norec, a) ty_tree =
+  insert_tree entry_name NR11 gsymbols pf action tree
 
-let insert_tree (type s trs trt p k a) ~warning entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree =
+let insert_tree (type s trs trt p k a) entry_name (gsymbols : (s, trs, p) ty_symbols) (pf : (p, k, a) rel_prod) (action : k) (tree : (s, trt, a) ty_tree) : (s, a) ty_mayrec_tree =
   let MayRecNR ar = and_symbols_tree gsymbols tree in
-  MayRecTree (insert_tree ~warning entry_name ar gsymbols pf action tree)
+  MayRecTree (insert_tree entry_name ar gsymbols pf action tree)
 
-let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_symbol =
+let srules (type self a) (rl : a ty_rules list) : (self, norec, a) ty_symbol =
   let rec retype_tree : type s a. (s, norec, a) ty_tree -> (self, norec, a) ty_tree =
     function
     | Node (NoRec3, {node = s; son = son; brother = bro}) ->
@@ -439,7 +457,7 @@ let srules (type self a) ~warning (rl : a ty_rules list) : (self, norec, a) ty_s
       (fun tree (TRules (symbols, action)) ->
         let symbols = retype_rule symbols in
         let AnyS (symbols, pf) = get_symbols symbols in
-        insert_tree_norec ~warning "" symbols pf action tree)
+        insert_tree_norec "" symbols pf action tree)
       DeadEnd rl
   in
   Stree t
@@ -449,19 +467,19 @@ let is_level_labelled n (Level lev) =
     Some n1 -> n = n1
   | None -> false
 
-let insert_level (type s tr p k) ~warning entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level =
+let insert_level (type s tr p k) entry_name (symbols : (s, tr, p) ty_symbols) (pf : (p, k, Loc.t -> s) rel_prod) (action : k) (slev : s ty_level) : s ty_level =
   match symbols with
   | TCns (_, Sself, symbols) ->
       let Level slev = slev in
       let RelS pf = pf in
-      let MayRecTree lsuffix = insert_tree ~warning entry_name symbols pf action slev.lsuffix in
+      let MayRecTree lsuffix = insert_tree entry_name symbols pf action slev.lsuffix in
       Level
       {assoc = slev.assoc; lname = slev.lname;
        lsuffix = lsuffix;
        lprefix = slev.lprefix}
   | _ ->
       let Level slev = slev in
-      let MayRecTree lprefix = insert_tree ~warning entry_name symbols pf action slev.lprefix in
+      let MayRecTree lprefix = insert_tree entry_name symbols pf action slev.lprefix in
       Level
       {assoc = slev.assoc; lname = slev.lname; lsuffix = slev.lsuffix;
        lprefix = lprefix}
@@ -475,34 +493,27 @@ let empty_lev lname assoc =
   Level
   {assoc = assoc; lname = lname; lsuffix = DeadEnd; lprefix = DeadEnd}
 
-let change_lev ~warning (Level lev) n lname assoc =
+let change_lev (Level lev) n lname assoc =
   let a =
     match assoc with
       None -> lev.assoc
     | Some a ->
       if a <> lev.assoc then
-        begin
-          match warning with
-          | None -> ()
-          | Some warn_fn ->
-            warn_fn ("<W> Changing associativity of level \""^n^"\"")
-        end;
-        a
+        Feedback.msg_warning (Pp.str ("<W> Changing associativity of level \""^n^"\""));
+      a
   in
-  begin match lname with
-    Some n ->
-      if lname <> lev.lname then
-        begin match warning with
-          | None -> ()
-          | Some warn_fn ->
-            warn_fn ("<W> Level label \""^n^"\" ignored")
-        end;
-  | None -> ()
+  begin
+    match lname with
+    | Some n ->
+      (* warning disabled; it was in the past *)
+      if false && lname <> lev.lname then
+        Feedback.msg_warning (Pp.str ("<W> Level label \""^n^"\" ignored"))
+    | None -> ()
   end;
   Level
   {assoc = a; lname = lev.lname; lsuffix = lev.lsuffix; lprefix = lev.lprefix}
 
-let get_level ~warning entry position levs =
+let get_level entry position levs =
   match position with
     Some First -> [], empty_lev, levs
   | Some Last -> levs, empty_lev, []
@@ -515,7 +526,7 @@ let get_level ~warning entry position levs =
             flush stderr;
             failwith "Grammar.extend"
         | lev :: levs ->
-            if is_level_labelled n lev then [], change_lev ~warning lev n, levs
+            if is_level_labelled n lev then [], change_lev lev n, levs
             else
               let (levs1, rlev, levs2) = get levs in lev :: levs1, rlev, levs2
       in
@@ -550,7 +561,7 @@ let get_level ~warning entry position levs =
       get levs
   | None ->
       match levs with
-        lev :: levs -> [], change_lev ~warning lev "<top>", levs
+        lev :: levs -> [], change_lev lev "<top>", levs
       | [] -> [], empty_lev, []
 
 let change_to_self0 (type s) (type trec) (type a) (entry : s ty_entry) : (s, trec, a) ty_symbol -> (s, a) ty_mayrec_symbol =
@@ -600,7 +611,7 @@ let insert_tokens gram symbols =
   in
   linsert symbols
 
-let levels_of_rules ~warning entry position rules =
+let levels_of_rules entry position rules =
   let elev =
     match entry.edesc with
       Dlevels elev -> elev
@@ -612,7 +623,7 @@ let levels_of_rules ~warning entry position rules =
   match rules with
   | [] -> elev
   | _ ->
-    let (levs1, make_lev, levs2) = get_level ~warning entry position elev in
+    let (levs1, make_lev, levs2) = get_level entry position elev in
     let (levs, _) =
       List.fold_left
         (fun (levs, make_lev) (lname, assoc, level) ->
@@ -623,7 +634,7 @@ let levels_of_rules ~warning entry position rules =
                   let MayRecRule symbols = change_to_self entry symbols in
                   let AnyS (symbols, pf) = get_symbols symbols in
                   insert_tokens egram symbols;
-                  insert_level ~warning entry.ename symbols pf action lev)
+                  insert_level entry.ename symbols pf action lev)
                lev level
            in
            lev :: levs, empty_lev)
@@ -1479,8 +1490,8 @@ let init_entry_functions entry =
        let f = continue_parser_of_entry entry in
        entry.econtinue <- f; f lev bp a strm)
 
-let extend_entry ~warning entry position rules =
-    let elev = levels_of_rules ~warning entry position rules in
+let extend_entry entry position rules =
+    let elev = levels_of_rules entry position rules in
     entry.edesc <- Dlevels elev; init_entry_functions entry
 
 (* Deleting a rule *)
@@ -1508,7 +1519,7 @@ module Parsable = struct
     { pa_chr_strm : char Stream.t
     ; pa_tok_strm : L.te Stream.t
     ; pa_loc_func : Plexing.location_function
-    }
+    ; lexer_state : L.State.t ref }
 
   let parse_parsable entry p =
     let efun = entry.estart 0 in
@@ -1544,9 +1555,26 @@ module Parsable = struct
       let loc = Stream.count cs, Stream.count cs + 1 in
       restore (); Ploc.raise (Ploc.make_unlined loc) exc
 
+  let parse_parsable e p =
+    L.State.set !(p.lexer_state);
+    try
+      let c = parse_parsable e p in
+      p.lexer_state := L.State.get ();
+      c
+    with Ploc.Exc (loc,e) ->
+      L.State.drop ();
+      let loc' = Loc.get_loc (Exninfo.info e) in
+      let loc = match loc' with None -> loc | Some loc -> loc in
+      Loc.raise ~loc e
+
   let make ?loc cs =
+    let lexer_state = ref (L.State.init ()) in
+    L.State.set !lexer_state;
     let (ts, lf) = L.tok_func ?loc cs in
-    {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf}
+    lexer_state := L.State.get ();
+    {pa_chr_strm = cs; pa_tok_strm = ts; pa_loc_func = lf; lexer_state}
+
+  let comments p = L.State.get_comments !(p.lexer_state)
 
 end
 
@@ -1557,6 +1585,7 @@ module Entry = struct
       econtinue =
         (fun _ _ _ (strm__ : _ Stream.t) -> raise Stream.Failure);
       edesc = Dlevels []}
+  let create = make
   let parse (e : 'a t) p : 'a =
     Parsable.parse_parsable e p
   let parse_token_stream (e : 'a t) ts : 'a =
@@ -1589,7 +1618,7 @@ module rec Symbol : sig
   val self : ('self, mayrec, 'self) t
   val next : ('self, mayrec, 'self) t
   val token : 'c pattern -> ('self, norec, 'c) t
-  val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+  val rules : 'a Rules.t list -> ('self, norec, 'a) t
 
 end = struct
 
@@ -1604,7 +1633,7 @@ end = struct
   let self = Sself
   let next = Snext
   let token tok = Stoken tok
-  let rules ~warning (t : 'a Rules.t list) = srules ~warning t
+  let rules (t : 'a Rules.t list) = srules t
 
 end and Rule : sig
 
@@ -1656,14 +1685,87 @@ 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_delete_rule e r =
+let safe_extend (e : 'a Entry.t) { pos; data } =
+  extend_entry e pos data
+
+let safe_delete_rule e (TProd (r,_act)) =
   let AnyS (symbols, _) = get_symbols r in
   delete_rule e symbols
 
+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 f0423a92af..33006f6f65 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -15,8 +15,7 @@
        rule "an entry cannot call an entry of another grammar" by
        normal OCaml typing. *)
 
-module type GLexerType = Plexing.Lexer
-   (** The input signature for the functor [Grammar.GMake]: [te] is the
+(** The input signature for the functor [Grammar.GMake]: [te] is the
        type of the tokens. *)
 
 type norec
@@ -29,6 +28,7 @@ module type S = sig
   module Parsable : sig
     type t
     val make : ?loc:Loc.t -> char Stream.t -> t
+    val comments : t -> ((int * int) * string) list
   end
 
   val tokens : string -> (string option * int) list
@@ -36,6 +36,7 @@ module type S = sig
   module Entry : sig
     type 'a t
     val make : string -> 'a t
+    val create : string -> 'a t (* compat *)
     val parse : 'a t -> Parsable.t -> 'a
     val name : 'a t -> string
     val of_parser : string -> (Plexing.location_function -> te Stream.t -> 'a) -> 'a t
@@ -60,7 +61,7 @@ module type S = sig
     val self : ('self, mayrec, 'self) t
     val next : ('self, mayrec, 'self) t
     val token : 'c pattern -> ('self, norec, 'c) t
-    val rules : warning:(string -> unit) option -> 'a Rules.t list -> ('self, norec, 'a) t
+    val rules : 'a Rules.t list -> ('self, norec, 'a) t
 
   end and Rule : sig
 
@@ -86,17 +87,37 @@ module type S = sig
     val make : ('a, _, 'f, Loc.t -> 'a) Rule.t -> 'f -> 'a t
   end
 
-  module Unsafe :
-  sig
+  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 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
+
+(* Interface private to clients  *)
+module type ExtS = sig
+
+  include S
+
+  val safe_extend : 'a Entry.t -> 'a extend_statement -> unit
+  val safe_delete_rule : 'a Entry.t -> 'a Production.t -> unit
+
+  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
+
 end
+
 (** Signature type of the functor [Grammar.GMake]. The types and
     functions are almost the same than in generic interface, but:
     -      Grammars are not values. Functions holding a grammar as parameter
@@ -107,5 +128,4 @@ end
       type (instead of (string * string)); the module parameter
       must specify a way to show them as (string * string) *)
 
-module GMake (L : GLexerType) :
-  S with type te = L.te and type 'c pattern = 'c L.pattern
+module GMake (L : Plexing.S) : ExtS with type te = L.te and type 'c pattern = 'c L.pattern
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index e881ab3350..ce3e38ff08 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -5,7 +5,7 @@
 type location_function = int -> Loc.t
 type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
 
-module type Lexer = sig
+module type S = sig
   type te
   type 'c pattern
   val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option
@@ -15,4 +15,15 @@ module type Lexer = sig
   val tok_removing : 'c pattern -> unit
   val tok_match : 'c pattern -> te -> 'c
   val tok_text : 'c pattern -> string
+
+  (* State for the comments, at some point we should make it functional *)
+  module State : sig
+    type t
+    val init : unit -> t
+    val set : t -> unit
+    val get : unit -> t
+    val drop : unit -> unit
+    val get_comments : t -> ((int * int) * string) list
+  end
+
 end
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 521eba7446..0c190af635 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -15,7 +15,7 @@ and location_function = int -> Loc.t
   (** The type of a function giving the location of a token in the
       source from the token number in the stream (starting from zero). *)
 
-module type Lexer = sig
+module type S = sig
   type te
   type 'c pattern
   val tok_pattern_eq : 'a pattern -> 'b pattern -> ('a, 'b) Util.eq option
@@ -25,4 +25,15 @@ module type Lexer = sig
   val tok_removing : 'c pattern -> unit
   val tok_match : 'c pattern -> te -> 'c
   val tok_text : 'c pattern -> string
+
+  (* State for the comments, at some point we should make it functional *)
+  module State : sig
+    type t
+    val init : unit -> t
+    val set : t -> unit
+    val get : unit -> t
+    val drop : unit -> unit
+    val get_comments : t -> ((int * int) * string) list
+  end
+
 end
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index a39da96a53..85640cabba 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -392,22 +392,6 @@ let comments = ref []
 let current_comment = Buffer.create 8192
 let between_commands = ref true
 
-(* The state of the lexer visible from outside *)
-type lexer_state = int option * string * bool * ((int * int) * string) list
-
-let init_lexer_state () = (None,"",true,[])
-let set_lexer_state (o,s,b,c) =
-  comment_begin := o;
-  Buffer.clear current_comment; Buffer.add_string current_comment s;
-  between_commands := b;
-  comments := c
-let get_lexer_state () =
-  (!comment_begin, Buffer.contents current_comment, !between_commands, !comments)
-let drop_lexer_state () =
-    set_lexer_state (init_lexer_state ())
-
-let get_comment_state (_,_,_,c) = c
-
 let real_push_char c = Buffer.add_char current_comment c
 
 (* Add a char if it is between two commands, if it is a newline or
@@ -851,6 +835,24 @@ module MakeLexer (Diff : sig val mode : bool end) = struct
   let tok_removing = (fun _ -> ())
   let tok_match = Tok.match_pattern
   let tok_text = token_text
+
+  (* The state of the lexer visible from outside *)
+  module State = struct
+
+    type t = int option * string * bool * ((int * int) * string) list
+
+    let init () = (None,"",true,[])
+    let set (o,s,b,c) =
+      comment_begin := o;
+      Buffer.clear current_comment; Buffer.add_string current_comment s;
+      between_commands := b;
+      comments := c
+    let get () =
+      (!comment_begin, Buffer.contents current_comment, !between_commands, !comments)
+    let drop () = set (init ())
+    let get_comments (_,_,_,c) = c
+
+  end
 end
 
 module Lexer = MakeLexer (struct let mode = false end)
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index 2c1284c4db..ac2c5bcfe2 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -55,7 +55,7 @@ val terminal_numeral : string -> NumTok.Unsigned.t Tok.p
 (** The lexer of Coq: *)
 
 module Lexer :
-  Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p
+  Gramlib.Plexing.S with type te = Tok.t and type 'c pattern = 'c Tok.p
 
 module Error : sig
   type t
@@ -63,15 +63,6 @@ module Error : sig
   val to_string : t -> string
 end
 
-(* Mainly for comments state, etc... *)
-type lexer_state
-
-val init_lexer_state : unit -> lexer_state
-val set_lexer_state : lexer_state -> unit
-val get_lexer_state : unit -> lexer_state
-val drop_lexer_state : unit -> unit
-val get_comment_state : lexer_state -> ((int * int) * string) list
-
 (** Create a lexer.  true enables alternate handling for computing diffs.
 It ensures that, ignoring white space, the concatenated tokens equal the input
 string.  Specifically:
@@ -81,5 +72,6 @@ as if it was unquoted, possibly becoming multiple tokens
 it was not in a comment, possibly becoming multiple tokens
 - return any unrecognized Ascii or UTF-8 character as a string
 *)
+
 module LexerDiff :
-  Gramlib.Grammar.GLexerType with type te = Tok.t and type 'c pattern = 'c Tok.p
+  Gramlib.Plexing.S with type te = Tok.t and type 'c pattern = 'c Tok.p
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 20297fa156..fadfb6c5f4 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -10,8 +10,6 @@
 
 (** Entry keys for constr notations *)
 
-type 'a entry = 'a Gramlib.Grammar.GMake(CLexer.Lexer).Entry.t
-
 type side = Left | Right
 
 type production_position =
@@ -77,36 +75,3 @@ type ('a,'b,'c) ty_user_symbol =
 | TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol
 | TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol
 | TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol
-
-(** {5 Type-safe grammar extension} *)
-
-(* Should be merged with gramlib's implementation *)
-
-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
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b3f997e1b3..5b0562fb0d 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -10,113 +10,11 @@
 
 open CErrors
 open Util
-open Extend
 open Genarg
 open Gramlib
 
 (** The parser of Coq *)
-module G : sig
-
-  include Grammar.S with type te = Tok.t and type 'c pattern = 'c Tok.p
-
-(* where Grammar.S
-
-module type S =
-  sig
-    type te = 'x;
-    type parsable = 'x;
-    value parsable : Stream.t char -> parsable;
-    value tokens : string -> list (string * int);
-    value glexer : Plexing.lexer te;
-    value set_algorithm : parse_algorithm -> unit;
-    module Entry :
-      sig
-        type e 'a = 'y;
-        value create : string -> e 'a;
-        value parse : e 'a -> parsable -> 'a;
-        value parse_token_stream : e 'a -> Stream.t te -> 'a;
-        value name : e 'a -> string;
-        value of_parser : string -> (Stream.t te -> 'a) -> e 'a;
-        value print : Format.formatter -> e 'a -> unit;
-        external obj : e 'a -> Gramext.g_entry te = "%identity";
-      end
-    ;
-    module Unsafe :
-      sig
-        value gram_reinit : Plexing.lexer te -> unit;
-        value clear_entry : Entry.e 'a -> unit;
-      end
-    ;
-    value extend :
-      Entry.e 'a -> option Gramext.position ->
-        list
-          (option string * option Gramext.g_assoc *
-           list (list (Gramext.g_symbol te) * Gramext.g_action)) ->
-        unit;
-    value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit;
-  end
-  *)
-
-  type coq_parsable
-
-  val coq_parsable : ?loc:Loc.t -> char Stream.t -> coq_parsable
-  val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> coq_parsable -> 'a
-
-  val comment_state : coq_parsable -> ((int * int) * string) list
-
-end with type 'a Entry.t = 'a Extend.entry = struct
-
-  include Grammar.GMake(CLexer.Lexer)
-
-  type coq_parsable = Parsable.t * CLexer.lexer_state ref
-
-  let coq_parsable ?loc c =
-    let state = ref (CLexer.init_lexer_state ()) in
-    CLexer.set_lexer_state !state;
-    let a = Parsable.make ?loc c in
-    state := CLexer.get_lexer_state ();
-    (a,state)
-
-  let entry_create = Entry.make
-
-  let entry_parse e (p,state) =
-    CLexer.set_lexer_state !state;
-    try
-      let c = Entry.parse e p in
-      state := CLexer.get_lexer_state ();
-      c
-    with Ploc.Exc (loc,e) ->
-      CLexer.drop_lexer_state ();
-      let loc' = Loc.get_loc (Exninfo.info e) in
-      let loc = match loc' with None -> loc | Some loc -> loc in
-      Loc.raise ~loc e
-
-  let comment_state (p,state) =
-    CLexer.get_comment_state !state
-
-end
-
-module Parsable =
-struct
-  type t = G.coq_parsable
-  let make = G.coq_parsable
-  let comment_state = G.comment_state
-end
-
-module Entry =
-struct
-
-  type 'a t = 'a Grammar.GMake(CLexer.Lexer).Entry.t
-
-  let create = G.Entry.make
-  let parse = G.entry_parse
-  let print = G.Entry.print
-  let of_parser = G.Entry.of_parser
-  let name = G.Entry.name
-  let parse_token_stream = G.Entry.parse_token_stream
-
-end
+include Grammar.GMake(CLexer.Lexer)
 
 module Lookahead =
 struct
@@ -187,100 +85,21 @@ end
     In [single_extend_statement], first two parameters are name and
     assoc iff a level is created *)
 
-(** Binding general entry keys to symbol *)
-
-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, Loc.t -> r) Extend.rule -> (s, tr, a, Loc.t -> 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 Extend.rules -> a G.Rules.t = function
-| Rules (r, act) ->
-  let symb = symbol_of_rule r in
-  G.Rules.make symb act
-
-(** 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 of_coq_production_rule : type a. a Extend.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)
-
 (** 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
 
 module EntryCommand = Dyn.Make ()
-module EntryData = struct type _ t = Ex : 'b G.Entry.t String.Map.t -> ('a * 'b) t end
+module EntryData = struct type _ t = Ex : 'b Entry.t String.Map.t -> ('a * 'b) t end
 module EntryDataMap = EntryCommand.Map(EntryData)
 
 type ext_kind =
   | ByGrammar of extend_rule
   | ByEXTEND of (unit -> unit) * (unit -> unit)
-  | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.Entry.t -> ext_kind
+  | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b Entry.t -> ext_kind
 
 (** The list of extensions *)
 
@@ -290,49 +109,37 @@ let camlp5_entries = ref EntryDataMap.empty
 
 (** Deletion *)
 
-let grammar_delete e (pos,rls) =
+let grammar_delete e { pos; data } =
   List.iter
     (fun (n,ass,lev) ->
-      List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
-    (List.rev rls)
+      List.iter (fun pil -> 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 ({ 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 = { pos = Some ext; data = [Some lev,Some a,[]] } in
+  safe_extend e ext
 
 (** Extension *)
 
 let grammar_extend e ext =
-  let ext = of_coq_extend_statement ext in
   let undo () = grammar_delete e ext in
-  let pos, ext = fix_extend_statement ext in
-  let redo () = G.safe_extend ~warning:None e pos ext in
+  let redo () = safe_extend 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 = fix_extend_statement (of_coq_extend_statement ext) in
-  G.safe_extend ~warning:None e pos ext
+  safe_extend e ext
 
 let grammar_extend_sync_reinit e reinit ext =
   camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
-  let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
-  G.safe_extend ~warning:None e pos ext
-
-(** The apparent parser of Coq; encapsulate G to keep track
-    of the extensions. *)
-
-module Gram =
-  struct
-    include G
-  end
+  safe_extend e ext
 
 (** Remove extensions
 
@@ -344,11 +151,11 @@ let rec remove_grammars n =
     match !camlp5_state with
        | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.")
        | ByGrammar (ExtendRuleReinit (g, reinit, ext)) :: t ->
-           grammar_delete_reinit g reinit (of_coq_extend_statement ext);
+           grammar_delete_reinit g reinit ext;
            camlp5_state := t;
            remove_grammars (n-1)
        | ByGrammar (ExtendRule (g, ext)) :: t ->
-           grammar_delete g (of_coq_extend_statement ext);
+           grammar_delete g ext;
            camlp5_state := t;
            remove_grammars (n-1)
        | ByEXTEND (undo,redo)::t ->
@@ -358,7 +165,7 @@ let rec remove_grammars n =
            redo();
            camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state
        | ByEntry (tag, name, e) :: t ->
-           G.Unsafe.clear_entry e;
+           Unsafe.clear_entry e;
            camlp5_state := t;
            let EntryData.Ex entries =
              try EntryDataMap.find tag !camlp5_entries
@@ -373,19 +180,19 @@ let make_rule r = [None, None, r]
 (** An entry that checks we reached the end of the input. *)
 
 let eoi_entry en =
-  let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
-  let symbs = G.Rule.next (G.Rule.next G.Rule.stop (G.Symbol.nterm en)) (G.Symbol.token Tok.PEOI) in
+  let e = Entry.make ((Entry.name en) ^ "_eoi") in
+  let symbs = Rule.next (Rule.next Rule.stop (Symbol.nterm en)) (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 = { pos = None; data = make_rule [Production.make symbs act] } in
+  safe_extend e ext;
   e
 
 let map_entry f en =
-  let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
-  let symbs = G.Rule.next G.Rule.stop (G.Symbol.nterm en) in
+  let e = Entry.make ((Entry.name en) ^ "_map") in
+  let symbs = Rule.next Rule.stop (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 = { pos = None; data = make_rule [Production.make symbs act] } in
+  safe_extend e ext;
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -393,7 +200,7 @@ let map_entry f en =
 
 let parse_string f ?loc x =
   let strm = Stream.of_string x in
-  Gram.entry_parse f (Gram.coq_parsable ?loc strm)
+  Entry.parse f (Parsable.make ?loc strm)
 
 type gram_universe = string
 
@@ -414,7 +221,7 @@ let get_univ u =
 
 let new_entry u s =
   let ename = u ^ ":" ^ s in
-  let e = Entry.create ename in
+  let e = Entry.make ename in
   e
 
 let make_gen_entry u s = new_entry u s
@@ -530,13 +337,11 @@ module Module =
     let module_type = Entry.create "module_type"
   end
 
-let epsilon_value (type s tr a) f (e : (s, tr, a) symbol) =
-  let s = symbol_of_prod_entry_key e in
-  let r = G.Production.make (G.Rule.next G.Rule.stop s) (fun x _ -> f x) in
-  let ext = [None, None, [r]] in
-  let entry = Gram.entry_create "epsilon" in
-  let warning msg = Feedback.msg_warning Pp.(str msg) in
-  let () = G.safe_extend ~warning:(Some warning) entry None ext in
+let epsilon_value (type s tr a) f (e : (s, tr, a) Symbol.t) =
+  let r = Production.make (Rule.next Rule.stop e) (fun x _ -> f x) in
+  let entry = Entry.make "epsilon" in
+  let ext = { pos = None; data = [None, None, [r]] } in
+  let () = safe_extend entry ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)
@@ -594,14 +399,14 @@ let extend_grammar_command tag g =
   let nb = List.length rules in
   grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
 
-let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.Entry.t list =
+let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Entry.t list =
   let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in
   let grammar_state = match !grammar_stack with
   | [] -> GramState.empty
   | (_, st) :: _ -> st
   in
   let (names, st) = modify g grammar_state in
-  let entries = List.map (fun name -> Gram.entry_create name) names in
+  let entries = List.map (fun name -> Entry.make name) names in
   let iter name e =
     camlp5_state := ByEntry (tag, name, e) :: !camlp5_state;
     let EntryData.Ex old =
@@ -627,7 +432,7 @@ let extend_dyn_grammar (e, _) = match e with
 
 (** Registering extra grammar *)
 
-type any_entry = AnyEntry : 'a Gram.Entry.t -> any_entry
+type any_entry = AnyEntry : 'a Entry.t -> any_entry
 
 let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 87c7f168ce..90088be307 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -9,30 +9,13 @@
 (************************************************************************)
 
 open Names
-open Extend
 open Genarg
 open Constrexpr
 open Libnames
 
 (** The parser of Coq *)
 
-module Parsable :
-sig
-  type t
-  val make : ?loc:Loc.t -> char Stream.t -> t
-  (* Get comment parsing information from the Lexer *)
-  val comment_state : t -> ((int * int) * string) list
-end
-
-module Entry : sig
-  type 'a t = 'a Extend.entry
-  val create : string -> 'a t
-  val parse : 'a t -> Parsable.t -> 'a
-  val print : Format.formatter -> 'a t -> unit
-  val of_parser : string -> (Gramlib.Plexing.location_function -> Tok.t Stream.t -> 'a) -> 'a t
-  val parse_token_stream : 'a t -> Tok.t Stream.t -> 'a
-  val name : 'a t -> string
-end
+include Gramlib.Grammar.S with type te = Tok.t and type 'a pattern = 'a Tok.p
 
 module Lookahead : sig
   type t
@@ -222,24 +205,11 @@ module Module :
     val module_type : module_ast Entry.t
   end
 
-val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self option
+(** {5 Type-safe grammar extension} *)
 
-(** {5 Extending the parser without synchronization} *)
+val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Symbol.t -> 'self option
 
-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
+(** {5 Extending the parser without synchronization} *)
 
 val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
@@ -257,6 +227,9 @@ 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
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4af5699317..4127d28bae 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -44,11 +44,11 @@ let coincide s pat off =
   !break
 
 let atactic n =
-  if n = 5 then Aentry Pltac.binder_tactic
-  else Aentryl (Pltac.tactic_expr, string_of_int n)
+  if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
+  else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
 
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
 
 (** Quite ad-hoc *)
 let get_tacentry n m =
@@ -57,8 +57,8 @@ let get_tacentry n m =
     && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
     && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
   in
-  if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
-  else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+  if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self)
+  else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.next)
   else EntryName (rawwit Tacarg.wit_tactic, atactic n)
 
 let get_separator = function
@@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with
 let rec prod_item_of_symbol lev = function
 | Extend.Ulist1 s ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Alist1 e)
+  EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1 e)
 | Extend.Ulist0 s ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Alist0 e)
+  EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0 e)
 | Extend.Ulist1sep (s, sep) ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep)))
+  EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
 | Extend.Ulist0sep (s, sep) ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep)))
+  EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
 | Extend.Uopt s ->
   let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
-  EntryName (Rawwit (OptArg typ), Aopt e)
+  EntryName (Rawwit (OptArg typ), Pcoq.Symbol.opt e)
 | Extend.Uentry arg ->
   let ArgT.Any tag = arg in
   let wit = ExtraArg tag in
-  EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit))
+  EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
 | Extend.Uentryl (s, n) ->
   let ArgT.Any tag = s in
   assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -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, { pos; data=[(None, None, [rules])]}) in
   ([r], state)
 
 let tactic_grammar =
@@ -399,23 +399,29 @@ let create_ltac_quotation name cast (e, l) =
   in
   let () = ltac_quotations := String.Set.add name !ltac_quotations in
   let entry = match l with
-  | None -> Aentry e
-  | Some l -> Aentryl (e, string_of_int l)
+  | None -> Pcoq.Symbol.nterm e
+  | Some l -> Pcoq.Symbol.nterml e (string_of_int l)
   in
 (*   let level = Some "1" in *)
   let level = None in
   let assoc = None in
   let rule =
-    Next (Next (Next (Next (Next (Stop,
-      Atoken (CLexer.terminal name)),
-      Atoken (CLexer.terminal ":")),
-      Atoken (CLexer.terminal "(")),
-      entry),
-      Atoken (CLexer.terminal ")"))
+    Pcoq.(
+      Rule.next
+        (Rule.next
+           (Rule.next
+              (Rule.next
+                 (Rule.next
+                    Rule.stop
+                    (Symbol.token (CLexer.terminal name)))
+                 (Symbol.token (CLexer.terminal ":")))
+              (Symbol.token (CLexer.terminal "(")))
+           entry)
+        (Symbol.token (CLexer.terminal ")")))
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
-  let gram = (level, assoc, [Rule (rule, action)]) in
-  Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
+  let gram = (level, assoc, [Pcoq.Production.make rule action]) in
+  Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
 
 (** Command *)
 
@@ -759,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 {pos=None; data=[(None, None, rules)]} in
     e
   in
   let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index d73d1f2d1a..3a6424ba9f 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -96,18 +96,17 @@ let tokenize_string s =
     else
       stream_tok ((Tok.extract_string true e) :: acc) str
   in
-  let st = CLexer.get_lexer_state () in
+  let st = CLexer.Lexer.State.get () in
   try
     let istr = Stream.of_string s in
     let lex = CLexer.LexerDiff.tok_func istr in
     let toks = stream_tok [] (fst lex) in
-    CLexer.set_lexer_state st;
+    CLexer.Lexer.State.set st;
     toks
   with exn ->
-    CLexer.set_lexer_state st;
+    CLexer.Lexer.State.set st;
     raise (Diff_Failure "Input string is not lexable");;
 
-
 type hyp_info = {
   idents: string list;
   rhs_pp: Pp.t;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 955630f40c..076796468f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -100,7 +100,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
     with
     | None ->
       input_cleanup ();
-      state, ids, Pcoq.Parsable.comment_state in_pa
+      state, ids, Pcoq.Parsable.comments in_pa
     | Some ast ->
       (* Printing of AST for -compile-verbose *)
       Option.iter (vernac_echo ?loc:ast.CAst.loc) in_echo;
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 5e04959e9a..57d59fc2ef 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -826,12 +826,12 @@ END
 
 let () =
 
-let open Extend in
 let open Tok in
-let (++) r s = Next (r, s) in
+let (++) r s = Pcoq.Rule.next r s in
 let rules = [
-  Rule (
-    Stop ++ Aentry test_dollar_ident ++ Atoken (PKEYWORD "$") ++ Aentry Prim.ident,
+  Pcoq.(
+    Production.make
+      (Rule.stop ++ Symbol.nterm test_dollar_ident ++ Symbol.token (PKEYWORD "$") ++ Symbol.nterm 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
@@ -839,8 +839,9 @@ let rules = [
     end
   );
 
-  Rule (
-    Stop ++ Aentry test_ampersand_ident ++ Atoken (PKEYWORD "&") ++ Aentry Prim.ident,
+  Pcoq.(
+    Production.make
+      (Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm 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_constr) tac in
@@ -848,9 +849,10 @@ let rules = [
     end
   );
 
-  Rule (
-    Stop ++ Atoken (PIDENT (Some "ltac2")) ++ Atoken (PKEYWORD ":") ++
-      Atoken (PKEYWORD "(") ++ Aentry tac2expr ++ Atoken (PKEYWORD ")"),
+  Pcoq.(
+    Production.make
+      (Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++
+       Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")"))
     begin fun _ tac _ _ _ loc ->
       let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
       CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
@@ -859,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 {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 38b05bed6b..2ed854c9f7 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1431,7 +1431,7 @@ let q_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0))
 let add_generic_scope s entry arg =
   let parse = function
   | [] ->
-    let scope = Extend.Aentry entry in
+    let scope = Pcoq.Symbol.nterm entry in
     let act x = CAst.make @@ CTacExt (arg, x) in
     Tac2entries.ScopeRule (scope, act)
   | arg -> scope_fail s arg
@@ -1442,14 +1442,14 @@ open CAst
 
 let () = add_scope "keyword" begin function
 | [SexprStr {loc;v=s}] ->
-  let scope = Extend.Atoken (Tok.PKEYWORD s) in
+  let scope = Pcoq.Symbol.token (Tok.PKEYWORD s) in
   Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
 | arg -> scope_fail "keyword" arg
 end
 
 let () = add_scope "terminal" begin function
 | [SexprStr {loc;v=s}] ->
-  let scope = Extend.Atoken (CLexer.terminal s) in
+  let scope = Pcoq.Symbol.token (CLexer.terminal s) in
   Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
 | arg -> scope_fail "terminal" arg
 end
@@ -1457,13 +1457,13 @@ end
 let () = add_scope "list0" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let scope = Extend.Alist0 scope in
+  let scope = Pcoq.Symbol.list0 scope in
   let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | [tok; SexprStr {v=str}] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let sep = Extend.Atoken (CLexer.terminal str) in
-  let scope = Extend.Alist0sep (scope, sep) in
+  let sep = Pcoq.Symbol.token (CLexer.terminal str) in
+  let scope = Pcoq.Symbol.list0sep scope sep false in
   let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "list0" arg
@@ -1472,13 +1472,13 @@ end
 let () = add_scope "list1" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let scope = Extend.Alist1 scope in
+  let scope = Pcoq.Symbol.list1 scope in
   let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | [tok; SexprStr {v=str}] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let sep = Extend.Atoken (CLexer.terminal str) in
-  let scope = Extend.Alist1sep (scope, sep) in
+  let sep = Pcoq.Symbol.token (CLexer.terminal str) in
+  let scope = Pcoq.Symbol.list1sep scope sep false in
   let act l = Tac2quote.of_list act l in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "list1" arg
@@ -1487,7 +1487,7 @@ end
 let () = add_scope "opt" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
-  let scope = Extend.Aopt scope in
+  let scope = Pcoq.Symbol.opt scope in
   let act opt = match opt with
   | None ->
     CAst.make @@ CTacCst (AbsKn (Other Core.c_none))
@@ -1500,7 +1500,7 @@ end
 
 let () = add_scope "self" begin function
 | [] ->
-  let scope = Extend.Aself in
+  let scope = Pcoq.Symbol.self in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "self" arg
@@ -1508,7 +1508,7 @@ end
 
 let () = add_scope "next" begin function
 | [] ->
-  let scope = Extend.Anext in
+  let scope = Pcoq.Symbol.next in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "next" arg
@@ -1517,12 +1517,12 @@ end
 let () = add_scope "tactic" begin function
 | [] ->
   (* Default to level 5 parsing *)
-  let scope = Extend.Aentryl (tac2expr, "5") in
+  let scope = Pcoq.Symbol.nterml tac2expr "5" in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | [SexprInt {loc;v=n}] as arg ->
   let () = if n < 0 || n > 6 then scope_fail "tactic" arg in
-  let scope = Extend.Aentryl (tac2expr, string_of_int n) in
+  let scope = Pcoq.Symbol.nterml tac2expr (string_of_int n) in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | arg -> scope_fail "tactic" arg
@@ -1543,12 +1543,12 @@ let () = add_scope "constr" (fun arg ->
         arg
     in
     let act e = Tac2quote.of_constr ~delimiters e in
-    Tac2entries.ScopeRule (Extend.Aentry Pcoq.Constr.constr, act)
+    Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
   )
 
 let add_expr_scope name entry f =
   add_scope name begin function
-  | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, f)
+  | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f)
   | arg -> scope_fail name arg
   end
 
@@ -1578,28 +1578,7 @@ let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
 
 (** seq scope, a bit hairy *)
 
-open Extend
-exception SelfSymbol
-
-let rec generalize_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
-  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
+open Pcoq
 
 type _ converter =
 | CvNil : (Loc.t -> raw_tacexpr) converter
@@ -1611,16 +1590,21 @@ 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, Extend.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) Rule.t * 'act converter -> seqrule
 
 let rec make_seq_rule = function
 | [] ->
-  Seqrule (Stop, CvNil)
+  Seqrule (Pcoq.Rule.stop, CvNil)
 | tok :: rem ->
   let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in
-  let scope = generalize_symbol scope in
+  let scope =
+    match Pcoq.generalize_symbol scope with
+    | None ->
+      CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules")
+    | Some scope -> scope
+  in
   let Seqrule (r, c) = make_seq_rule rem in
-  let r = NextNoRec (r, scope) in
+  let r = Pcoq.Rule.next_norec r scope in
   let f = match tok with
   | SexprStr _ -> None (* Leave out mere strings *)
   | _ -> Some f
@@ -1629,11 +1613,8 @@ let rec make_seq_rule = function
 
 let () = add_scope "seq" begin fun toks ->
   let scope =
-    try
-      let Seqrule (r, c) = make_seq_rule (List.rev toks) in
-      Arules [Rules (r, apply c [])]
-    with SelfSymbol ->
-      CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules")
+    let Seqrule (r, c) = make_seq_rule (List.rev toks) in
+    Pcoq.(Symbol.rules [Rules.make r (apply c [])])
   in
   Tac2entries.ScopeRule (scope, (fun e -> e))
 end
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index e9945794d3..ebc63ddd01 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) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
 
 type scope_interpretation = sexpr list -> scope_rule
 
@@ -583,7 +583,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.PIDENT (Some str)), (fun _ -> v_unit))
+  ScopeRule (Pcoq.Symbol.token (Tok.PIDENT (Some str)), (fun _ -> v_unit))
 | tok ->
   let loc = loc_of_token tok in
   CErrors.user_err ?loc (str "Invalid parsing token")
@@ -611,19 +611,19 @@ type synext = {
 
 type krule =
 | KRule :
-  (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Extend.rule *
+  (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.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
-| [] -> KRule (Extend.Stop, fun k loc -> k loc [])
+| [] -> KRule (Pcoq.Rule.stop, fun k loc -> k loc [])
 | TacNonTerm (na, ScopeRule (scope, inj)) :: tok ->
   let KRule (rule, act) = get_rule tok in
-  let rule = Extend.Next (rule, scope) in
+  let rule = Pcoq.Rule.next rule scope in
   let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in
   KRule (rule, act)
 | TacTerm t :: tok ->
   let KRule (rule, act) = get_rule tok in
-  let rule = Extend.Next (rule, Extend.Atoken (CLexer.terminal t)) in
+  let rule = Pcoq.(Rule.next rule (Symbol.token (CLexer.terminal t))) in
   let act k _ = act k in
   KRule (rule, act)
 
@@ -637,13 +637,13 @@ let perform_notation syn st =
     let bnd = List.map map args in
     CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp)
   in
-  let rule = Extend.Rule (rule, act mk) in
+  let rule = Pcoq.Production.make rule (act mk) in
   let lev = match syn.synext_lev with
   | None -> None
   | 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.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 fed43a4dd5..edad118dc9 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) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.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 5dae389a62..fdc8b1ba4c 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -325,51 +325,48 @@ let is_binder_level custom (custom',from) e = match e with
 | _ -> false
 
 let make_sep_rules = function
-  | [tk] -> Atoken tk
+  | [tk] ->
+    Pcoq.Symbol.token tk
   | tkl ->
-  let rec mkrule : 'a Tok.p list -> 'a rules = function
-  | [] -> Rules (Stop, fun _ -> (* dropped anyway: *) "")
-  | tkn :: rem ->
-    let Rules (r, f) = mkrule rem in
-    let r = NextNoRec (r, Atoken tkn) in
-    Rules (r, fun _ -> f)
-  in
-  let r = mkrule (List.rev tkl) in
-  Arules [r]
+    let r = Pcoq.mk_rule (List.rev tkl) in
+    Pcoq.Symbol.rules [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, Gramlib.Grammar.norec, 'a) Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, Gramlib.Grammar.mayrec, 'a) 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 then (* Prevent self *) MayRecNo (Aentryl (target_entry custom forpat, "200"))
-  else if is_self custom from p then MayRecMay Aself
+  if is_binder_level custom from p
+  then
+    (* Prevent self *)
+    MayRecNo (Pcoq.Symbol.nterml (target_entry custom forpat) "200")
+  else if is_self custom from p then MayRecMay Pcoq.Symbol.self
   else
     let g = target_entry custom forpat in
     let lev = adjust_level custom assoc from p in
     begin match lev with
-    | DefaultLevel -> MayRecNo (Aentry g)
-    | NextLevel -> MayRecMay Anext
-    | NumLevel lev -> MayRecNo (Aentryl (g, string_of_int lev))
+    | DefaultLevel -> MayRecNo (Pcoq.Symbol.nterm g)
+    | NextLevel -> MayRecMay Pcoq.Symbol.next
+    | NumLevel lev -> MayRecNo (Pcoq.Symbol.nterml g (string_of_int lev))
     end
 
 let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
 | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
 | TTConstrList (s, typ', [], forpat) ->
   begin match symbol_of_target s typ' assoc from forpat with
-  | MayRecNo s -> MayRecNo (Alist1 s)
-  | MayRecMay s -> MayRecMay (Alist1 s) end
+  | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1 s)
+  | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1 s) end
 | TTConstrList (s, typ', tkl, forpat) ->
   begin match symbol_of_target s typ' assoc from forpat with
-  | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl))
-  | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end
-| TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p))
-| TTClosedBinderList [] -> MayRecNo (Alist1 (Aentry Constr.binder))
-| TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl))
-| TTName -> MayRecNo (Aentry Prim.name)
-| TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
-| TTBigint -> MayRecNo (Aentry Prim.bignat)
-| TTReference -> MayRecNo (Aentry Constr.global)
+  | MayRecNo s -> MayRecNo (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false)
+  | MayRecMay s -> MayRecMay (Pcoq.Symbol.list1sep s (make_sep_rules tkl) false) end
+| TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p))
+| TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder))
+| TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
+| TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name)
+| TTOpenBinderList -> MayRecNo (Pcoq.Symbol.nterm Constr.open_binders)
+| TTBigint -> MayRecNo (Pcoq.Symbol.nterm Prim.bignat)
+| TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global)
 
 let interp_entry forpat e = match e with
 | ETProdName -> TTAny TTName
@@ -461,22 +458,22 @@ 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, Extend.norec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
-| MayRecRMay : ('s, Extend.mayrec, 'a, 'r) Extend.rule -> ('s, 'a, 'r) mayrec_rule
+| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, Gramlib.Grammar.mayrec, 'a, 'r) 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 Stop
+| TyStop -> MayRecRNo Rule.stop
 | TyMark (_, _, _, r) -> ty_erase r
 | TyNext (rem, TyTerm tok) ->
    begin match ty_erase rem with
-   | MayRecRNo rem -> MayRecRMay (Next (rem, Atoken tok))
-   | MayRecRMay rem -> MayRecRMay (Next (rem, Atoken tok)) end
+   | MayRecRNo rem -> MayRecRMay (Rule.next rem (Symbol.token tok))
+   | MayRecRMay rem -> MayRecRMay (Rule.next rem (Symbol.token tok)) end
 | TyNext (rem, TyNonTerm (_, _, s, _)) ->
    begin match ty_erase rem, s with
-   | MayRecRNo rem, MayRecNo s -> MayRecRMay (Next (rem, s))
-   | MayRecRNo rem, MayRecMay s -> MayRecRMay (Next (rem, s))
-   | MayRecRMay rem, MayRecNo s -> MayRecRMay (Next (rem, s))
-   | MayRecRMay rem, MayRecMay s -> MayRecRMay (Next (rem, s)) end
+   | MayRecRNo rem, MayRecNo s -> MayRecRMay (Rule.next rem s)
+   | MayRecRNo rem, MayRecMay s -> MayRecRMay (Rule.next rem s)
+   | MayRecRMay rem, MayRecNo s -> MayRecRMay (Rule.next rem s)
+   | MayRecRMay rem, MayRecMay s -> MayRecRMay (Rule.next rem s) end
 
 type ('self, 'r) any_ty_rule =
 | AnyTyRule : ('self, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -504,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 = { pos; data = [(name, p4assoc, [])] } in
   match reinit with
   | None ->
     ExtendRule (target_entry where forpat, empty)
@@ -522,7 +519,13 @@ let rec pure_sublevels' assoc from forpat level = function
    let rem = pure_sublevels' assoc from forpat level rem in
    let push where p rem =
      match symbol_of_target where p assoc from forpat with
-     | MayRecNo (Aentryl (_,i)) when different_levels (fst from,level) (where,i) -> (where,int_of_string i) :: rem
+     | MayRecNo sym ->
+       (match Pcoq.level_of_nonterm sym with
+        | None -> rem
+        | Some i ->
+          if different_levels (fst from,level) (where,i) then
+            (where,int_of_string i) :: rem
+          else rem)
      | _ -> rem in
    (match e with
    | ETProdPattern i -> push InConstrEntry (NumLevel i,InternalProd) rem
@@ -553,14 +556,15 @@ let extend_constr state forpat ng =
     let act = ty_eval r (make_act forpat ng.notgram_notation) empty in
     let rule =
       let r = match ty_erase r with
-        | MayRecRNo symbs -> Rule (symbs, act)
-        | MayRecRMay symbs -> Rule (symbs, act) in
+        | MayRecRNo symbs -> Pcoq.Production.make symbs act
+        | MayRecRMay symbs -> Pcoq.Production.make symbs act
+      in
       name, p4assoc, [r] in
     let r = match reinit with
       | None ->
-        ExtendRule (entry, (pos, [rule]))
+        ExtendRule (entry, { pos; data = [rule]})
       | Some reinit ->
-        ExtendRuleReinit (entry, reinit, (pos, [rule]))
+        ExtendRuleReinit (entry, reinit, { pos; data = [rule]})
     in
     (accu @ empty_rules @ [r], state)
   in
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 793aad6b24..bda1401bc9 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,14 +19,14 @@ 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) Symbol.t) Loc.located -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
 type ('self, 'tr, _, 'r) ty_rule =
-| TyStop : ('self, Extend.norec, 'r, 'r) ty_rule
-| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Extend.symbol * 'b ty_arg option ->
-  ('self, Extend.mayrec, 'b -> 'a, 'r) ty_rule
+| TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) Symbol.t * 'b ty_arg option ->
+  ('self, Gramlib.Grammar.mayrec, 'b -> 'a, 'r) ty_rule
 
 type ('self, 'r) any_ty_rule =
 | AnyTyRule : ('self, _, 'act, Loc.t -> 'r) ty_rule -> ('self, 'r) any_ty_rule
@@ -35,7 +35,7 @@ let rec ty_rule_of_gram = function
 | [] -> AnyTyRule TyStop
 | GramTerminal s :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
-  let tok = Atoken (CLexer.terminal s) in
+  let tok = Pcoq.Symbol.token (CLexer.terminal s) in
   let r = TyNext (rem, tok, None) in
   AnyTyRule r
 | GramNonTerminal (_, (t, tok)) :: rem ->
@@ -44,9 +44,9 @@ 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) Extend.rule = function
-| TyStop -> Extend.Stop
-| TyNext (rem, tok, _) -> Extend.Next (ty_erase rem, tok)
+let rec ty_erase : type s tr a r. (s, tr, a, r) ty_rule -> (s, tr, a, r) Pcoq.Rule.t = function
+| TyStop -> Pcoq.Rule.stop
+| TyNext (rem, tok, _) -> Pcoq.Rule.next (ty_erase rem) tok
 
 type 'r gen_eval = Loc.t -> raw_generic_argument list -> 'r
 
@@ -62,7 +62,7 @@ let make_rule f prod =
   let symb = ty_erase ty_rule in
   let f loc l = f loc (List.rev l) in
   let act = ty_eval ty_rule f in
-  Extend.Rule (symb, act)
+  Pcoq.Production.make symb act
 
 let rec proj_symbol : type a b c. (a, b, c) ty_user_symbol -> (a, b, c) genarg_type = function
 | TUentry a -> ExtraArg a
@@ -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 { pos=None; data=[None, None, rules]}
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 7f6656b079..15f415ca3b 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) Extend.symbol) Loc.located -> 's grammar_prod_item
+      ('s, _, 'a) Pcoq.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 Extend.production_rule
+  'a grammar_prod_item list -> 'a Pcoq.Production.t
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 08625b41a6..f4cb1adfe8 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -51,14 +51,13 @@ module Vernac_ =
     let noedit_mode = gec_vernac "noedit_command"
 
     let () =
-      let open Extend in
       let act_vernac v loc = Some v in
       let act_eoi _ loc = None in
       let rule = [
-        Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
-        Rule (Next (Stop, Aentry vernac_control), act_vernac);
+        Pcoq.(Production.make (Rule.next Rule.stop (Symbol.token Tok.PEOI)) act_eoi);
+        Pcoq.(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 {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 0e8202da9f..1920c276af 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -166,15 +166,15 @@ 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, Extend.norec, a) Extend.symbol =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.norec, a) Pcoq.Symbol.t =
   let open Extend in function
-| TUlist1 l -> Alist1 (untype_user_symbol l)
-| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s))
-| TUlist0 l -> Alist0 (untype_user_symbol l)
-| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s))
-| TUopt o -> Aopt (untype_user_symbol o)
-| TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a))
-| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i)
+  | TUlist1 l -> Pcoq.Symbol.list1 (untype_user_symbol l)
+  | TUlist1sep (l, s) -> Pcoq.Symbol.list1sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false
+  | TUlist0 l -> Pcoq.Symbol.list0 (untype_user_symbol l)
+  | TUlist0sep (l, s) -> Pcoq.Symbol.list0sep (untype_user_symbol l) (Pcoq.Symbol.token (CLexer.terminal s)) false
+  | TUopt o -> Pcoq.Symbol.opt (untype_user_symbol o)
+  | TUentry a -> Pcoq.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
+  | TUentryl (a, i) -> Pcoq.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i)
 
 let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function
 | TyNil -> []
@@ -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 Extend.production_rule list
+| Arg_rules of 'a Pcoq.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.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 90c00415d4..0d0ebc1086 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 Extend.production_rule list
+| Arg_rules of 'a Pcoq.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. *)