[parsing] Remove redundant interfaces from Pcoq

There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.

A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.

20 files changed, 70 insertions, 110 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index 0ef7fca41f..81e7e4d148 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -91,7 +91,7 @@ let set_doc doc = ide_doc := Some doc
 
 let add ((s,eid),(sid,verbose)) =
   let doc = get_doc () in
-  let pa = Pcoq.Parsable.make (Stream.of_string s) in
+  let pa = Pcoq.G.Parsable.make (Stream.of_string s) in
   match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
   | None -> assert false (* s is not an empty string *)
   | Some ast ->
@@ -127,13 +127,13 @@ let edit_at id =
  * be removed in the next version of the protocol.
  *)
 let query (route, (s,id)) =
-  let pa = Pcoq.Parsable.make (Stream.of_string s) in
+  let pa = Pcoq.G.Parsable.make (Stream.of_string s) in
   let doc = get_doc () in
   Stm.query ~at:id ~doc ~route pa
 
 let annotate phrase =
   let doc = get_doc () in
-  let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
+  let pa = Pcoq.G.Parsable.make (Stream.of_string phrase) in
   match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with
   | None -> Richpp.richpp_of_pp 78 (Pp.mt ())
   | Some ast ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 7d301e75bd..8f3c1e029c 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -15,9 +15,6 @@ open Gramlib
 
 (** The parser of Coq *)
 
-type norec = Gramlib.Grammar.norec
-type mayrec = Gramlib.Grammar.mayrec
-
 module G : sig
 
   include Grammar.S
@@ -25,9 +22,6 @@ module G : sig
      and type 'c pattern = 'c Tok.p
 
   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.t option
-  val mk_rule : 'a Tok.p list -> string Rules.t
 
 end = struct
 
@@ -92,11 +86,6 @@ end = struct
   let mk_rule = G_.mk_rule
 end
 
-module Parsable = struct
-  include G.Parsable
-  let comment_state = G.comment_state
-end
-
 module Entry = struct
   include G.Entry
   let create = make
@@ -121,7 +110,7 @@ struct
 
   let to_entry s (lk : t) =
     let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in
-    Entry.of_parser s run
+    G.Entry.of_parser s run
 
   let (>>) (lk1 : t) lk2 tok n strm = match lk1 tok n strm with
   | None -> None
@@ -171,8 +160,6 @@ end
     In [single_extend_statement], first two parameters are name and
     assoc iff a level is created *)
 
-(** Binding general entry keys to symbol *)
-
 (** Type of reinitialization data *)
 type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
 
@@ -230,14 +217,6 @@ let grammar_extend_sync_reinit e reinit ext =
   camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
   G.safe_extend ~warning:None e ext
 
-(** The apparent parser of Coq; encapsulate G to keep track
-    of the extensions. *)
-
-module Gram =
-  struct
-    include G
-  end
-
 (** Remove extensions
 
    [n] is the number of extended entries (not the number of Grammar commands!)
@@ -277,21 +256,21 @@ 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 e = G.Entry.make ((G.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 act = fun _ x loc -> x in
   let warning msg = Feedback.msg_warning Pp.(str msg) in
   let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
-  Gram.safe_extend ~warning:(Some warning) e ext;
+  G.safe_extend ~warning:(Some warning) e ext;
   e
 
 let map_entry f en =
-  let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
+  let e = G.Entry.make ((G.Entry.name en) ^ "_map") in
   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
   let ext = { G.pos = None; data = make_rule [G.Production.make symbs act] } in
-  Gram.safe_extend ~warning:(Some warning) e ext;
+  G.safe_extend ~warning:(Some warning) e ext;
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -320,14 +299,14 @@ let get_univ u =
 
 let new_entry u s =
   let ename = u ^ ":" ^ s in
-  let e = Entry.create ename in
+  let e = G.Entry.make ename in
   e
 
 let make_gen_entry u s = new_entry u s
 
 module GrammarObj =
 struct
-  type ('r, _, _) obj = 'r Entry.t
+  type ('r, _, _) obj = 'r G.Entry.t
   let name = "grammar"
   let default _ = None
 end
@@ -350,7 +329,7 @@ let genarg_grammar x =
   check_compatibility x;
   Grammar.obj x
 
-let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t =
+let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a G.Entry.t =
   let e = new_entry u s in
   let Rawwit t = etyp in
   let () = Grammar.register0 t e in
@@ -499,7 +478,7 @@ 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 G.Entry.t list =
   let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in
   let grammar_state = match !grammar_stack with
   | [] -> GramState.empty
@@ -532,7 +511,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 G.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 e12a1cc11b..0352c1d55b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -15,22 +15,18 @@ 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 G : sig
+
+  include Gramlib.Grammar.S
+
+  val comment_state : Parsable.t -> ((int * int) * string) list
+
+end with type te = Tok.t and type 'a pattern = 'a Tok.p
 
 module Entry : sig
-  type 'a t
+  type 'a t = 'a G.Entry.t
   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
 
 module Lookahead : sig
@@ -223,21 +219,6 @@ module Module :
 
 (** {5 Type-safe grammar extension} *)
 
-type norec = Gramlib.Grammar.norec
-type mayrec = Gramlib.Grammar.mayrec
-
-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.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
-
 val epsilon_value : ('a -> 'self) -> ('self, _, 'a) G.Symbol.t -> 'self option
 
 (** {5 Extending the parser without synchronization} *)
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 5a26ac8827..bec83411c1 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -62,7 +62,7 @@ open Extraargs
 
 (* idem for (x1..xn:t) [n^2 complexity but exceptional use] *)
 let check_for_coloneq =
-  Pcoq.Entry.of_parser "lpar_id_colon"
+  Pcoq.G.Entry.of_parser "lpar_id_colon"
     (fun _ strm ->
       let rec skip_to_rpar p n =
         match List.last (Stream.npeek n strm) with
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 442b40221b..c3396584a4 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -263,16 +263,16 @@ let negate_parser f tok x =
   | Some _ -> raise Stream.Failure
 
 let test_not_ssrslashnum =
-  Pcoq.Entry.of_parser
+  Pcoq.G.Entry.of_parser
     "test_not_ssrslashnum" (negate_parser test_ssrslashnum10)
 let test_ssrslashnum00 =
-  Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
+  Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum00
 let test_ssrslashnum10 =
-  Pcoq.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
+  Pcoq.G.Entry.of_parser "test_ssrslashnum10" test_ssrslashnum10
 let test_ssrslashnum11 =
-  Pcoq.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
+  Pcoq.G.Entry.of_parser "test_ssrslashnum11" test_ssrslashnum11
 let test_ssrslashnum01 =
-  Pcoq.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
+  Pcoq.G.Entry.of_parser "test_ssrslashnum01" test_ssrslashnum01
 
 }
 
@@ -459,7 +459,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "@" -> xWithAt
   | _ -> xNoFlag
 
-let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 (* New kinds of terms *)
 
@@ -470,7 +470,7 @@ let input_term_annotation _ strm =
   | Tok.KEYWORD "@" :: _ -> `At
   | _ -> `None
 let term_annotation =
-  Pcoq.Entry.of_parser "term_annotation" input_term_annotation
+  Pcoq.G.Entry.of_parser "term_annotation" input_term_annotation
 
 (* terms *)
 
@@ -811,7 +811,7 @@ let reject_ssrhid _ strm =
       | _ -> ())
   | _ -> ()
 
-let test_nohidden = Pcoq.Entry.of_parser "test_ssrhid" reject_ssrhid
+let test_nohidden = Pcoq.G.Entry.of_parser "test_ssrhid" reject_ssrhid
 
 let rec reject_binder crossed_paren k tok s =
   match
@@ -825,7 +825,7 @@ let rec reject_binder crossed_paren k tok s =
   | Some (Tok.KEYWORD ")") when crossed_paren -> raise Stream.Failure
   | _ -> if crossed_paren then () else raise Stream.Failure
 
-let _test_nobinder = Pcoq.Entry.of_parser "test_nobinder" (reject_binder false 0)
+let _test_nobinder = Pcoq.G.Entry.of_parser "test_nobinder" (reject_binder false 0)
 
 }
 
@@ -1659,7 +1659,7 @@ let ssr_id_of_string loc s =
   ^ "Scripts with explicit references to anonymous variables are fragile."))
     end; Id.of_string s
 
-let ssr_null_entry = Pcoq.Entry.of_parser "ssr_null" (fun _ _ -> ())
+let ssr_null_entry = Pcoq.G.Entry.of_parser "ssr_null" (fun _ _ -> ())
 
 }
 
@@ -2382,7 +2382,7 @@ let test_ssr_rw_syntax =
     match Util.stream_nth 0 strm with
     | Tok.KEYWORD key when List.mem key.[0] [lbrace; '['; '/'] -> ()
     | _ -> raise Stream.Failure in
-  Pcoq.Entry.of_parser "test_ssr_rw_syntax" test
+  Pcoq.G.Entry.of_parser "test_ssr_rw_syntax" test
 
 }
 
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 33e523a4a4..59abf80dc5 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -70,7 +70,7 @@ let input_ssrtermkind _ strm = match Util.stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
   | Tok.KEYWORD "@" -> '@'
   | _ -> ' '
-let ssrtermkind = Pcoq.Entry.of_parser "ssrtermkind" input_ssrtermkind
+let ssrtermkind = Pcoq.G.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
 }
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 2c27d63b82..88da3c747f 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -93,7 +93,7 @@ val new_doc  : stm_init_options -> doc * Stateid.t
     be the case if an error was raised at parsing time). *)
 val parse_sentence :
   doc:doc -> Stateid.t ->
-  entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a
+  entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.G.Parsable.t -> 'a
 
 (* Reminder: A parsable [pa] is constructed using
    [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
@@ -119,7 +119,7 @@ val get_proof : doc:doc -> Stateid.t -> Proof.t option
    throwing away side effects except messages. Feedback will
    be sent with [report_with], which defaults to the dummy state id *)
 val query : doc:doc ->
-  at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit
+  at:Stateid.t -> route:Feedback.route_id -> Pcoq.G.Parsable.t -> unit
 
 (* [edit_at id] is issued to change the editing zone.  [`NewTip] is returned if
    the requested id is the new document tip hence the document portion following
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b8acdd3af1..0d9edb248b 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -23,7 +23,7 @@ type input_buffer = {
   mutable str : Bytes.t; (* buffer of already read characters *)
   mutable len : int;    (* number of chars in the buffer *)
   mutable bols : int list; (* offsets in str of beginning of lines *)
-  mutable tokens : Pcoq.Parsable.t; (* stream of tokens *)
+  mutable tokens : Pcoq.G.Parsable.t; (* stream of tokens *)
   mutable start : int } (* stream count of the first char of the buffer *)
 
 (* Double the size of the buffer. *)
@@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf =
   ibuf.str <- Bytes.empty;
   ibuf.len <- 0;
   ibuf.bols <- [];
-  ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf));
+  ibuf.tokens <- Pcoq.G.Parsable.make (Stream.from (prompt_char doc ic ibuf));
   ibuf.start <- 0
 
 (* Functions to print underlined locations from an input buffer. *)
@@ -230,7 +230,7 @@ let top_buffer =
     str = Bytes.empty;
     len = 0;
     bols = [];
-    tokens = Pcoq.Parsable.make (Stream.of_list []);
+    tokens = Pcoq.G.Parsable.make (Stream.of_list []);
     start = 0 }
 
 let set_prompt prompt =
@@ -247,7 +247,7 @@ let parse_to_dot =
     | Tok.EOI -> ()
     | _ -> dot tok st
   in
-  Pcoq.Entry.of_parser "Coqtoplevel.dot" dot
+  Pcoq.G.Entry.of_parser "Coqtoplevel.dot" dot
 
 (* If an error occurred while parsing, we try to read the input until a dot
    token is encountered.
@@ -255,7 +255,7 @@ let parse_to_dot =
 
 let rec discard_to_dot () =
   try
-    Pcoq.Entry.parse parse_to_dot top_buffer.tokens
+    Pcoq.G.Entry.parse parse_to_dot top_buffer.tokens
   with
     | CLexer.Error.E _ -> discard_to_dot ()
     | e when CErrors.noncritical e -> ()
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 1eafc70530..b07f3e5c57 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -18,7 +18,7 @@ type input_buffer = {
   mutable str : Bytes.t; (** buffer of already read characters *)
   mutable len : int;    (** number of chars in the buffer *)
   mutable bols : int list; (** offsets in str of beginning of lines *)
-  mutable tokens : Pcoq.Parsable.t; (** stream of tokens *)
+  mutable tokens : Pcoq.G.Parsable.t; (** stream of tokens *)
   mutable start : int } (** stream count of the first char of the buffer *)
 
 (** The input buffer of stdin. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 955630f40c..ce4b85c75f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -88,7 +88,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
   let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
 
   let in_pa =
-    Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile file))
+    Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile file))
       (Stream.of_channel in_chan) in
   let open State in
 
@@ -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.G.comment_state 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/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 0946c88228..920be6db5b 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) G.Rule.t * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) G.Rule.t * 'act converter -> seqrule
 
 let rec make_seq_rule = function
 | [] ->
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 88bcf1d477..7a52f53dc0 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) G.Symbol.t -> ('s, 'a) mayrec_symbol
-| MayRecMay : ('s, mayrec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecNo : ('s, Gramlib.Grammar.norec, 'a) G.Symbol.t -> ('s, 'a) mayrec_symbol
+| MayRecMay : ('s, Gramlib.Grammar.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) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
-| MayRecRMay : ('s, mayrec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRNo : ('s, Gramlib.Grammar.norec, 'a, 'r) G.Rule.t -> ('s, 'a, 'r) mayrec_rule
+| MayRecRMay : ('s, Gramlib.Grammar.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
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 00a239f56e..981de78162 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -24,9 +24,9 @@ type '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.G.Symbol.t * 'b ty_arg option ->
-  ('self, Pcoq.mayrec, 'b -> 'a, 'r) ty_rule
+| TyStop : ('self, Gramlib.Grammar.norec, 'r, 'r) ty_rule
+| TyNext : ('self, _, 'a, 'r) ty_rule * ('self, _, 'b) G.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
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 475d5c31f7..38e57a310a 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -46,7 +46,7 @@ let entry_buf = Buffer.create 64
 let pr_entry e =
   let () = Buffer.clear entry_buf in
   let ft = Format.formatter_of_buffer entry_buf in
-  let () = Pcoq.Entry.print ft e in
+  let () = Pcoq.G.Entry.print ft e in
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
@@ -55,7 +55,7 @@ let pr_registered_grammar name =
   | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.")
   | entries ->
     let pr_one (Pcoq.AnyEntry e) =
-      str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++
+      str "Entry " ++ str (Pcoq.G.Entry.name e) ++ str " is" ++ fnl () ++
       pr_entry e
     in
     prlist pr_one entries
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index 2130a398e9..8d0dcbf0fe 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -169,7 +169,7 @@ let suggest_variable env id =
 let value = ref None
 
 let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
-let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
+let using_from_string us = Pcoq.G.Entry.parse G_vernac.section_subset_expr (Pcoq.G.Parsable.make (Stream.of_string us))
 
 let proof_using_opt_name = ["Default";"Proof";"Using"]
 let () =
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 9a9c96064d..26364ed075 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -65,8 +65,8 @@ module Vernac_ =
       | Some ename -> find_proof_mode ename
 
     let command_entry =
-      Pcoq.Entry.of_parser "command_entry"
-        (fun _ strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
+      Pcoq.G.Entry.of_parser "command_entry"
+        (fun _ strm -> Pcoq.G.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm)
 
   end
 
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index ac4d33c926..4008c3d799 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, Pcoq.norec, a) Pcoq.G.Symbol.t =
+let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, Gramlib.Grammar.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
-| TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l)
-| TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
-| TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o)
-| TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
-| TUentryl (a, i) -> Pcoq.G.Symbol.nterml (Pcoq.genarg_grammar (Genarg.ExtraArg a)) (string_of_int i)
+  | 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
+  | TUlist0 l -> Pcoq.G.Symbol.list0 (untype_user_symbol l)
+  | TUlist0sep (l, s) -> Pcoq.G.Symbol.list0sep (untype_user_symbol l) (Pcoq.G.Symbol.token (CLexer.terminal s)) false
+  | TUopt o -> Pcoq.G.Symbol.opt (untype_user_symbol o)
+  | TUentry a -> Pcoq.G.Symbol.nterm (Pcoq.genarg_grammar (Genarg.ExtraArg a))
+  | TUentryl (a, i) -> Pcoq.G.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 -> []
@@ -193,7 +193,7 @@ let vernac_extend ~command ?classifier ?entry ext =
     | None ->
       let e = match entry with
       | None -> "COMMAND"
-      | Some e -> Pcoq.Entry.name e
+      | Some e -> Pcoq.G.Entry.name e
       in
       let msg = Printf.sprintf "\
         Vernac entry \"%s\" misses a classifier. \
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 15a19c06c2..6b7b2c2691 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -183,12 +183,12 @@ and vernac_load ~verbosely fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = Util.open_utf8_file_in longfname in
-    Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
+    Pcoq.G.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
   (* Parsing loop *)
   let v_mod = if verbosely then Flags.verbosely else Flags.silently in
   let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
       (fun po ->
-         match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
+         match Pcoq.G.Entry.parse (Pvernac.main_entry proof_mode) po with
          | Some x -> x
          | None -> raise End_of_input) in
   let rec load_loop ~stack =
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 6846826bfa..49486b889d 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -19,7 +19,7 @@ module Parser = struct
   let parse ps entry pa =
     Pcoq.unfreeze ps;
     Flags.with_option Flags.we_are_parsing
-      (fun () -> Pcoq.Entry.parse entry pa)
+      (fun () -> Pcoq.G.Entry.parse entry pa)
       ()
 
 end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 7607f8373a..ed1b76b618 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -14,7 +14,7 @@ module Parser : sig
   val init : unit -> state
   val cur_state : unit -> state
 
-  val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a
+  val parse : state -> 'a Pcoq.Entry.t -> Pcoq.G.Parsable.t -> 'a
 
 end