Merge PR #7898: Remove camlp4 remains

28 files changed, 245 insertions, 278 deletions

diff --git a/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh b/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh
new file mode 100644
index 000000000..9c4c905fa
--- /dev/null
+++ b/dev/ci/user-overlays/07898-ppedrot-rm-campl4-remains.sh
@@ -0,0 +1,8 @@
+_OVERLAY_BRANCH=rm-campl4-remains
+
+if [ "$CI_PULL_REQUEST" = "7898" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    pidetop_CI_BRANCH="$_OVERLAY_BRANCH"
+    pidetop_CI_GITURL=https://github.com/ppedrot/pidetop
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6d5023405..1eea2443f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -88,6 +88,11 @@ Primitive number parsers
   have been split over three files (plugins/syntax/positive_syntax.ml,
   plugins/syntax/n_syntax.ml, plugins/syntax/z_syntax.ml).
 
+Parsing
+
+- Manual uses of the Pcoq.Gram module have been deprecated. Wrapper modules
+  Pcoq.Entry and Pcoq.Parsable were introduced to replace it.
+
 ### Unit testing
 
   The test suite now allows writing unit tests against OCaml code in the Coq
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 6fb004061..0c3328ee0 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -80,7 +80,7 @@ let set_doc doc = ide_doc := Some doc
 
 let add ((s,eid),(sid,verbose)) =
   let doc = get_doc () in
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  let pa = Pcoq.Parsable.make (Stream.of_string s) in
   let loc_ast = Stm.parse_sentence ~doc sid pa in
   let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
   set_doc doc;
@@ -113,14 +113,14 @@ let edit_at id =
  * be removed in the next version of the protocol.
  *)
 let query (route, (s,id)) =
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  let pa = Pcoq.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 {CAst.loc;v=ast} =
-    let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
+    let pa = Pcoq.Parsable.make (Stream.of_string phrase) in
     Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
   in
   (* XXX: Width should be a parameter of annotate... *)
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 997ea78e6..6726603e6 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -86,24 +86,15 @@ module type S =
   type internal_entry = Tok.t Gramext.g_entry
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
-  type production_rule = symbol list * action
-  type single_extend_statement =
-      string option * Gramext.g_assoc option * production_rule list
-  type extend_statement =
-      Gramext.position option * single_extend_statement list
   type coq_parsable
 
-  val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
+  val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
   val action : 'a -> action
   val entry_create : string -> 'a entry
   val entry_parse : 'a entry -> coq_parsable -> 'a
-  val entry_print : Format.formatter -> 'a entry -> unit
 
   val comment_state : coq_parsable -> ((int * int) * string) list
 
-  val srules' : production_rule list -> symbol
-  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
-
 end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
 
   include Grammar.GMake(CLexer)
@@ -112,15 +103,10 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
   type internal_entry = Tok.t Gramext.g_entry
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
-  type production_rule = symbol list * action
-  type single_extend_statement =
-      string option * Gramext.g_assoc option * production_rule list
-  type extend_statement =
-      Gramext.position option * single_extend_statement list
 
   type coq_parsable = parsable * CLexer.lexer_state ref
 
-  let parsable ?(file=Loc.ToplevelInput) c =
+  let coq_parsable ?(file=Loc.ToplevelInput) c =
     let state = ref (CLexer.init_lexer_state file) in
     CLexer.set_lexer_state !state;
     let a = parsable c in
@@ -145,11 +131,23 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
   let comment_state (p,state) =
     CLexer.get_comment_state !state
 
-  let entry_print ft x = Entry.print ft x
+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).Entry.e
 
-  (* Not used *)
-  let srules' = Gramext.srules
-  let parse_tokens_after_filter = Entry.parse_token
+  let create = G.Entry.create
+  let parse = G.entry_parse
+  let print = G.Entry.print
 
 end
 
@@ -246,7 +244,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Aentryl (e, n) ->
     Symbols.snterml (G.Entry.obj e, n)
   | Arules rs ->
-    G.srules' (List.map symbol_of_rules rs)
+    Gramext.srules (List.map symbol_of_rules rs)
 
 and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
 | Stop -> fun accu -> accu
@@ -364,14 +362,14 @@ let make_rule r = [None, None, r]
 (** An entry that checks we reached the end of the input. *)
 
 let eoi_entry en =
-  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
+  let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
   let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
   let act = Gram.action (fun _ x loc -> x) in
   uncurry (Gram.extend e) (None, make_rule [symbs, act]);
   e
 
 let map_entry f en =
-  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
+  let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
   let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
   let act = Gram.action (fun x loc -> f x) in
   uncurry (Gram.extend e) (None, make_rule [symbs, act]);
@@ -381,7 +379,7 @@ let map_entry f en =
    (use eoi_entry) *)
 
 let parse_string f x =
-  let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
+  let strm = Stream.of_string x in Gram.entry_parse f (Gram.coq_parsable strm)
 
 type gram_universe = string
 
@@ -402,14 +400,14 @@ let get_univ u =
 
 let new_entry u s =
   let ename = u ^ ":" ^ s in
-  let e = Gram.entry_create ename in
+  let e = Entry.create ename in
   e
 
 let make_gen_entry u s = new_entry u s
 
 module GrammarObj =
 struct
-  type ('r, _, _) obj = 'r Gram.entry
+  type ('r, _, _) obj = 'r Entry.t
   let name = "grammar"
   let default _ = None
 end
@@ -419,7 +417,7 @@ module Grammar = Register(GrammarObj)
 let register_grammar = Grammar.register0
 let genarg_grammar = Grammar.obj
 
-let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
+let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t =
   let e = new_entry u s in
   let Rawwit t = etyp in
   let () = Grammar.register0 t e in
@@ -431,38 +429,38 @@ module Prim =
   struct
     let gec_gen n = make_gen_entry uprim n
 
-    (* Entries that can be referred via the string -> Gram.entry table *)
+    (* Entries that can be referred via the string -> Entry.t table *)
     (* Typically for tactic or vernac extensions *)
     let preident = gec_gen "preident"
     let ident = gec_gen "ident"
     let natural = gec_gen "natural"
     let integer = gec_gen "integer"
-    let bigint = Gram.entry_create "Prim.bigint"
+    let bigint = Entry.create "Prim.bigint"
     let string = gec_gen "string"
-    let lstring = Gram.entry_create "Prim.lstring"
+    let lstring = Entry.create "Prim.lstring"
     let reference = make_gen_entry uprim "reference"
-    let by_notation = Gram.entry_create "by_notation"
-    let smart_global = Gram.entry_create "smart_global"
+    let by_notation = Entry.create "by_notation"
+    let smart_global = Entry.create "smart_global"
 
     (* parsed like ident but interpreted as a term *)
     let var = gec_gen "var"
 
-    let name = Gram.entry_create "Prim.name"
-    let identref = Gram.entry_create "Prim.identref"
-    let univ_decl = Gram.entry_create "Prim.univ_decl"
-    let ident_decl = Gram.entry_create "Prim.ident_decl"
-    let pattern_ident = Gram.entry_create "pattern_ident"
-    let pattern_identref = Gram.entry_create "pattern_identref"
+    let name = Entry.create "Prim.name"
+    let identref = Entry.create "Prim.identref"
+    let univ_decl = Entry.create "Prim.univ_decl"
+    let ident_decl = Entry.create "Prim.ident_decl"
+    let pattern_ident = Entry.create "pattern_ident"
+    let pattern_identref = Entry.create "pattern_identref"
 
     (* A synonym of ident - maybe ident will be located one day *)
-    let base_ident = Gram.entry_create "Prim.base_ident"
+    let base_ident = Entry.create "Prim.base_ident"
 
-    let qualid = Gram.entry_create "Prim.qualid"
-    let fullyqualid = Gram.entry_create "Prim.fullyqualid"
-    let dirpath = Gram.entry_create "Prim.dirpath"
+    let qualid = Entry.create "Prim.qualid"
+    let fullyqualid = Entry.create "Prim.fullyqualid"
+    let dirpath = Entry.create "Prim.dirpath"
 
-    let ne_string = Gram.entry_create "Prim.ne_string"
-    let ne_lstring = Gram.entry_create "Prim.ne_lstring"
+    let ne_string = Entry.create "Prim.ne_string"
+    let ne_lstring = Entry.create "Prim.ne_lstring"
 
   end
 
@@ -470,7 +468,7 @@ module Constr =
   struct
     let gec_constr = make_gen_entry uconstr
 
-    (* Entries that can be referred via the string -> Gram.entry table *)
+    (* Entries that can be referred via the string -> Entry.t table *)
     let constr = gec_constr "constr"
     let operconstr = gec_constr "operconstr"
     let constr_eoi = eoi_entry constr
@@ -481,29 +479,29 @@ module Constr =
     let universe_level = make_gen_entry uconstr "universe_level"
     let sort = make_gen_entry uconstr "sort"
     let sort_family = make_gen_entry uconstr "sort_family"
-    let pattern = Gram.entry_create "constr:pattern"
+    let pattern = Entry.create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
-    let closed_binder = Gram.entry_create "constr:closed_binder"
-    let binder = Gram.entry_create "constr:binder"
-    let binders = Gram.entry_create "constr:binders"
-    let open_binders = Gram.entry_create "constr:open_binders"
-    let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
-    let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
-    let record_declaration = Gram.entry_create "constr:record_declaration"
-    let appl_arg = Gram.entry_create "constr:appl_arg"
+    let closed_binder = Entry.create "constr:closed_binder"
+    let binder = Entry.create "constr:binder"
+    let binders = Entry.create "constr:binders"
+    let open_binders = Entry.create "constr:open_binders"
+    let binders_fixannot = Entry.create "constr:binders_fixannot"
+    let typeclass_constraint = Entry.create "constr:typeclass_constraint"
+    let record_declaration = Entry.create "constr:record_declaration"
+    let appl_arg = Entry.create "constr:appl_arg"
   end
 
 module Module =
   struct
-    let module_expr = Gram.entry_create "module_expr"
-    let module_type = Gram.entry_create "module_type"
+    let module_expr = Entry.create "module_expr"
+    let module_type = Entry.create "module_type"
   end
 
 let epsilon_value f e =
   let r = Rule (Next (Stop, e), fun x _ -> f x) in
   let ext = of_coq_extend_statement (None, [None, None, [r]]) in
-  let entry = G.entry_create "epsilon" in
+  let entry = Gram.entry_create "epsilon" in
   let () = uncurry (G.extend entry) ext in
   try Some (parse_string entry "") with _ -> None
 
@@ -608,7 +606,7 @@ let () =
 
 (** Registering extra grammar *)
 
-type any_entry = AnyEntry : 'a Gram.entry -> 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 154de1221..029c43713 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -16,82 +16,40 @@ open Libnames
 
 (** The parser of Coq *)
 
+(** DO NOT USE EXTENSION FUNCTIONS IN THIS MODULE.
+    We only have it here to work with Camlp5. Handwritten grammar extensions
+    should use the safe [Pcoq.grammar_extend] function below. *)
 module Gram : sig
 
   include Grammar.S with type te = Tok.t
 
-(* Where Grammar.S is
-
-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 : 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 'a entry = 'a Entry.e
+  [@@ocaml.deprecated "Use [Pcoq.Entry.t]"]
 
-*)
+  [@@@ocaml.warning "-3"]
 
-  type 'a entry = 'a Entry.e
-  type internal_entry = Tok.t Gramext.g_entry
-  type symbol = Tok.t Gramext.g_symbol
-  type action = Gramext.g_action
-  type production_rule = symbol list * action
-  type single_extend_statement =
-      string option * Gramext.g_assoc option * production_rule list
-  type extend_statement =
-      Gramext.position option * single_extend_statement list
-
-  type coq_parsable
-
-  val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
-  val action : 'a -> action
   val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> coq_parsable -> 'a
-  val entry_print : Format.formatter -> 'a entry -> unit
-
-  (* Get comment parsing information from the Lexer *)
-  val comment_state : coq_parsable -> ((int * int) * string) list
+  [@@ocaml.deprecated "Use [Pcoq.Entry.create]"]
 
   val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit
 
-  (* Apparently not used *)
-  val srules' : production_rule list -> symbol
-  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
+  [@@@ocaml.warning "+3"]
 
 end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
 
-module Symbols : sig
+module Parsable :
+sig
+  type t
+  val make : ?file:Loc.source -> char Stream.t -> t
+  (* Get comment parsing information from the Lexer *)
+  val comment_state : t -> ((int * int) * string) list
+end
 
-  val stoken : Tok.t -> Gram.symbol
-  val snterm : Gram.internal_entry -> Gram.symbol
+module Entry : sig
+  type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+  val create : string -> 'a t
+  val parse : 'a t -> Parsable.t -> 'a
+  val print : Format.formatter -> 'a t -> unit
 end
 
 (** The parser of Coq is built from three kinds of rule declarations:
@@ -175,86 +133,86 @@ val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
 (** Parse a string *)
 
-val parse_string : 'a Gram.entry -> string -> 'a
-val eoi_entry : 'a Gram.entry -> 'a Gram.entry
-val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry
+val parse_string : 'a Entry.t -> string -> 'a
+val eoi_entry : 'a Entry.t -> 'a Entry.t
+val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t
 
 type gram_universe
 
 val get_univ : string -> gram_universe
 val create_universe : string -> gram_universe
 
-val new_entry : gram_universe -> string -> 'a Gram.entry
+val new_entry : gram_universe -> string -> 'a Entry.t
 
 val uprim : gram_universe
 val uconstr : gram_universe
 val utactic : gram_universe
 
 
-val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit
-val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry
+val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t -> unit
+val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t
 
 val create_generic_entry : gram_universe -> string ->
-  ('a, rlevel) abstract_argument_type -> 'a Gram.entry
+  ('a, rlevel) abstract_argument_type -> 'a Entry.t
 
 module Prim :
   sig
     open Names
     open Libnames
-    val preident : string Gram.entry
-    val ident : Id.t Gram.entry
-    val name : lname Gram.entry
-    val identref : lident Gram.entry
-    val univ_decl : universe_decl_expr Gram.entry
-    val ident_decl : ident_decl Gram.entry
-    val pattern_ident : Id.t Gram.entry
-    val pattern_identref : lident Gram.entry
-    val base_ident : Id.t Gram.entry
-    val natural : int Gram.entry
-    val bigint : Constrexpr.raw_natural_number Gram.entry
-    val integer : int Gram.entry
-    val string : string Gram.entry
-    val lstring : lstring Gram.entry
-    val reference : qualid Gram.entry
-    val qualid : qualid Gram.entry
-    val fullyqualid : Id.t list CAst.t Gram.entry
-    val by_notation : (string * string option) Gram.entry
-    val smart_global : qualid or_by_notation Gram.entry
-    val dirpath : DirPath.t Gram.entry
-    val ne_string : string Gram.entry
-    val ne_lstring : lstring Gram.entry
-    val var : lident Gram.entry
+    val preident : string Entry.t
+    val ident : Id.t Entry.t
+    val name : lname Entry.t
+    val identref : lident Entry.t
+    val univ_decl : universe_decl_expr Entry.t
+    val ident_decl : ident_decl Entry.t
+    val pattern_ident : Id.t Entry.t
+    val pattern_identref : lident Entry.t
+    val base_ident : Id.t Entry.t
+    val natural : int Entry.t
+    val bigint : Constrexpr.raw_natural_number Entry.t
+    val integer : int Entry.t
+    val string : string Entry.t
+    val lstring : lstring Entry.t
+    val reference : qualid Entry.t
+    val qualid : qualid Entry.t
+    val fullyqualid : Id.t list CAst.t Entry.t
+    val by_notation : (string * string option) Entry.t
+    val smart_global : qualid or_by_notation Entry.t
+    val dirpath : DirPath.t Entry.t
+    val ne_string : string Entry.t
+    val ne_lstring : lstring Entry.t
+    val var : lident Entry.t
   end
 
 module Constr :
   sig
-    val constr : constr_expr Gram.entry
-    val constr_eoi : constr_expr Gram.entry
-    val lconstr : constr_expr Gram.entry
-    val binder_constr : constr_expr Gram.entry
-    val operconstr : constr_expr Gram.entry
-    val ident : Id.t Gram.entry
-    val global : qualid Gram.entry
-    val universe_level : Glob_term.glob_level Gram.entry
-    val sort : Glob_term.glob_sort Gram.entry
-    val sort_family : Sorts.family Gram.entry
-    val pattern : cases_pattern_expr Gram.entry
-    val constr_pattern : constr_expr Gram.entry
-    val lconstr_pattern : constr_expr Gram.entry
-    val closed_binder : local_binder_expr list Gram.entry
-    val binder : local_binder_expr list Gram.entry (* closed_binder or variable *)
-    val binders : local_binder_expr list Gram.entry (* list of binder *)
-    val open_binders : local_binder_expr list Gram.entry
-    val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry
-    val typeclass_constraint : (lname * bool * constr_expr) Gram.entry
-    val record_declaration : constr_expr Gram.entry
-    val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry
+    val constr : constr_expr Entry.t
+    val constr_eoi : constr_expr Entry.t
+    val lconstr : constr_expr Entry.t
+    val binder_constr : constr_expr Entry.t
+    val operconstr : constr_expr Entry.t
+    val ident : Id.t Entry.t
+    val global : qualid Entry.t
+    val universe_level : Glob_term.glob_level Entry.t
+    val sort : Glob_term.glob_sort Entry.t
+    val sort_family : Sorts.family Entry.t
+    val pattern : cases_pattern_expr Entry.t
+    val constr_pattern : constr_expr Entry.t
+    val lconstr_pattern : constr_expr Entry.t
+    val closed_binder : local_binder_expr list Entry.t
+    val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
+    val binders : local_binder_expr list Entry.t (* list of binder *)
+    val open_binders : local_binder_expr list Entry.t
+    val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t
+    val typeclass_constraint : (lname * bool * constr_expr) Entry.t
+    val record_declaration : constr_expr Entry.t
+    val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t
   end
 
 module Module :
   sig
-    val module_expr : module_ast Gram.entry
-    val module_type : module_ast Gram.entry
+    val module_expr : module_ast Entry.t
+    val module_type : module_ast Entry.t
   end
 
 val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
@@ -264,7 +222,7 @@ val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
 type gram_reinit = gram_assoc * gram_position
 (** Type of reinitialization data *)
 
-val grammar_extend : 'a Gram.entry -> gram_reinit option ->
+val grammar_extend : 'a Entry.t -> gram_reinit option ->
   'a Extend.extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
@@ -280,7 +238,7 @@ type 'a grammar_command
     marshallable. *)
 
 type extend_rule =
-| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule
 
 type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 (** Grammar extension entry point. Given some ['a] and a current grammar state,
@@ -310,7 +268,7 @@ val parser_summary_tag : frozen_t Summary.Dyn.tag
 
 (** Registering grammars by name *)
 
-type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+type any_entry = AnyEntry : 'a Entry.t -> any_entry
 
 val register_grammars_by_name : string -> any_entry list -> unit
 val find_grammars_by_name : string -> any_entry list
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 737147884..e477b12cd 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -14,12 +14,12 @@ open Constrexpr
 open Glob_term
 
 val wit_orient : bool Genarg.uniform_genarg_type
-val orient : bool Pcoq.Gram.entry
+val orient : bool Pcoq.Entry.t
 val pr_orient : bool -> Pp.t
 
 val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
 
-val occurrences : (int list Locus.or_var) Pcoq.Gram.entry
+val occurrences : (int list Locus.or_var) Pcoq.Entry.t
 val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type
 val pr_occurrences : int list Locus.or_var -> Pp.t
 val occurrences_of : int list -> Locus.occurrences
@@ -46,8 +46,8 @@ val wit_casted_constr :
   Tacexpr.glob_constr_and_expr,
   EConstr.t) Genarg.genarg_type
 
-val glob : constr_expr Pcoq.Gram.entry
-val lglob : constr_expr Pcoq.Gram.entry
+val glob : constr_expr Pcoq.Entry.t
+val lglob : constr_expr Pcoq.Entry.t
 
 type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
 
@@ -55,10 +55,10 @@ type loc_place = lident gen_place
 type place = Id.t gen_place
 
 val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
-val hloc : loc_place Pcoq.Gram.entry
+val hloc : loc_place Pcoq.Entry.t
 val pr_hloc : loc_place -> Pp.t
 
-val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
+val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Entry.t
 val wit_by_arg_tac :
   (raw_tactic_expr option,
   glob_tactic_expr option,
@@ -68,13 +68,13 @@ val pr_by_arg_tac :
   (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
   raw_tactic_expr option -> Pp.t
 
-val test_lpar_id_colon : unit Pcoq.Gram.entry
+val test_lpar_id_colon : unit Pcoq.Entry.t
 
 val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
 
 (** Spiwack: Primitive for retroknowledge registration *)
 
-val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
+val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
 val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
 
 val wit_in_clause :
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 620f14707..9d86f21d4 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -46,10 +46,10 @@ let reference_to_id qid =
     CErrors.user_err ?loc:qid.CAst.loc
       (str "This expression should be a simple identifier.")
 
-let tactic_mode = Gram.entry_create "vernac:tactic_command"
+let tactic_mode = Entry.create "vernac:tactic_command"
 
 let new_entry name =
-  let e = Gram.entry_create name in
+  let e = Entry.create name in
   e
 
 let toplevel_selector = new_entry "vernac:toplevel_selector"
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index e9711268c..759bb62fd 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -11,11 +11,10 @@
 open Pcoq
 
 (* Main entry for extensions *)
-let simple_tactic = Gram.entry_create "tactic:simple_tactic"
+let simple_tactic = Entry.create "tactic:simple_tactic"
 
-let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name)
+let make_gen_entry _ name = Entry.create ("tactic:" ^ name)
 
-(* Entries that can be referred via the string -> Gram.entry table *)
 (* Typically for tactic user extensions *)
 let open_constr =
   make_gen_entry utactic "open_constr"
@@ -23,7 +22,7 @@ let constr_with_bindings =
   make_gen_entry utactic "constr_with_bindings"
 let bindings =
   make_gen_entry utactic "bindings"
-let hypident = Gram.entry_create "hypident"
+let hypident = Entry.create "hypident"
 let constr_may_eval = make_gen_entry utactic "constr_may_eval"
 let constr_eval = make_gen_entry utactic "constr_eval"
 let uconstr =
@@ -40,7 +39,7 @@ let clause_dft_concl =
 
 
 (* Main entries for ltac *)
-let tactic_arg = Gram.entry_create "tactic:tactic_arg"
+let tactic_arg = Entry.create "tactic:tactic_arg"
 let tactic_expr = make_gen_entry utactic "tactic_expr"
 let binder_tactic = make_gen_entry utactic "binder_tactic"
 
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index c5aa542fd..9bff98b6c 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -17,22 +17,22 @@ open Tacexpr
 open Genredexpr
 open Tactypes
 
-val open_constr : constr_expr Gram.entry
-val constr_with_bindings : constr_expr with_bindings Gram.entry
-val bindings : constr_expr bindings Gram.entry
-val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
-val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
-val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
-val uconstr : constr_expr Gram.entry
-val quantified_hypothesis : quantified_hypothesis Gram.entry
-val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
-val int_or_var : int Locus.or_var Gram.entry
-val simple_tactic : raw_tactic_expr Gram.entry
-val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
-val in_clause : Names.lident Locus.clause_expr Gram.entry
-val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry
-val tactic_arg : raw_tactic_arg Gram.entry
-val tactic_expr : raw_tactic_expr Gram.entry
-val binder_tactic : raw_tactic_expr Gram.entry
-val tactic : raw_tactic_expr Gram.entry
-val tactic_eoi : raw_tactic_expr Gram.entry
+val open_constr : constr_expr Entry.t
+val constr_with_bindings : constr_expr with_bindings Entry.t
+val bindings : constr_expr bindings Entry.t
+val hypident : (Names.lident * Locus.hyp_location_flag) Entry.t
+val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t
+val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t
+val uconstr : constr_expr Entry.t
+val quantified_hypothesis : quantified_hypothesis Entry.t
+val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t
+val int_or_var : int Locus.or_var Entry.t
+val simple_tactic : raw_tactic_expr Entry.t
+val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
+val in_clause : Names.lident Locus.clause_expr Entry.t
+val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
+val tactic_arg : raw_tactic_arg Entry.t
+val tactic_expr : raw_tactic_expr Entry.t
+val binder_tactic : raw_tactic_expr Entry.t
+val tactic : raw_tactic_expr Entry.t
+val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 9bba9ba71..f873631ff 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -55,7 +55,7 @@ val add_ml_tactic_notation : ml_tactic_name -> level:int ->
 (** {5 Tactic Quotations} *)
 
 val create_ltac_quotation : string ->
-  ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
+  ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit
 (** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
     Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
     generates an argument using [f] on the entry parsed by [e]. *)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 6b183dab1..8b9c94f2d 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1408,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with
     CErrors.user_err ?loc (str "expected \"first\"")
   | _, _ -> arg
 
-let ssrorelse = Gram.entry_create "ssrorelse"
+let ssrorelse = Entry.create "ssrorelse"
 GEXTEND Gram
   GLOBAL: ssrorelse ssrseqarg;
   ssrseqidx: [
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 7cd3751ce..862a93765 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -12,11 +12,11 @@
 
 open Ltac_plugin
 
-val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
+val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
 
-val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
+val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
 
diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli
index bb5161a0e..588a1a3ea 100644
--- a/plugins/ssrmatching/g_ssrmatching.mli
+++ b/plugins/ssrmatching/g_ssrmatching.mli
@@ -5,13 +5,13 @@ open Genarg
 open Ssrmatching
 
 (** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *)
-val cpattern         : cpattern Pcoq.Gram.entry
+val cpattern         : cpattern Pcoq.Entry.t
 val wit_cpattern     : cpattern uniform_genarg_type
 
 (** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *)
-val lcpattern         : cpattern Pcoq.Gram.entry
+val lcpattern         : cpattern Pcoq.Entry.t
 val wit_lcpattern     : cpattern uniform_genarg_type
 
 (** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
-val rpattern         : rpattern Pcoq.Gram.entry
+val rpattern         : rpattern Pcoq.Entry.t
 val wit_rpattern     : rpattern uniform_genarg_type
diff --git a/stm/stm.ml b/stm/stm.ml
index 0aed88a53..e15b6048b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2976,7 +2976,7 @@ let parse_sentence ~doc sid pa =
        str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur.");
   Flags.with_option Flags.we_are_parsing (fun () ->
       try
-        match Pcoq.Gram.entry_parse Pvernac.main_entry pa with
+        match Pcoq.Entry.parse Pvernac.main_entry pa with
         | None            -> raise End_of_input
         | Some (loc, cmd) -> CAst.make ~loc cmd
       with e when CErrors.noncritical e ->
diff --git a/stm/stm.mli b/stm/stm.mli
index aed7274d0..50e7f0609 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -92,11 +92,11 @@ val new_doc  : stm_init_options -> doc * Stateid.t
 
 (** [parse_sentence sid pa] Reads a sentence from [pa] with parsing
    state [sid] Returns [End_of_input] if the stream ends *)
-val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable ->
+val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t ->
   Vernacexpr.vernac_control CAst.t
 
 (* Reminder: A parsable [pa] is constructed using
-   [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *)
+   [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
 
 exception End_of_input
 
@@ -114,7 +114,7 @@ val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
    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.Gram.coq_parsable -> unit
+  at:Stateid.t -> route:Feedback.route_id -> Pcoq.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 d7ede1c2e..7ae15ac10 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.Gram.coq_parsable; (* stream of tokens *)
+  mutable tokens : Pcoq.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.Gram.parsable (Stream.from (prompt_char doc ic ibuf));
+  ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf));
   ibuf.start <- 0
 
 (* Functions to print underlined locations from an input buffer. *)
@@ -228,7 +228,7 @@ let top_buffer =
     str = Bytes.empty;
     len = 0;
     bols = [];
-    tokens = Pcoq.Gram.parsable (Stream.of_list []);
+    tokens = Pcoq.Parsable.make (Stream.of_list []);
     start = 0 }
 
 let set_prompt prompt =
@@ -253,7 +253,7 @@ let parse_to_dot =
 
 let rec discard_to_dot () =
   try
-    Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens
+    Pcoq.Entry.parse parse_to_dot top_buffer.tokens
   with
     | Token.Error _ | CLexer.Error.E _ -> discard_to_dot ()
     | Stm.End_of_input -> raise Stm.End_of_input
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 5c07a8bf3..b11f13d3c 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 begining of lines *)
-  mutable tokens : Pcoq.Gram.coq_parsable; (** stream of tokens *)
+  mutable tokens : Pcoq.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/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 53d3eef23..5aba3d6b0 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -21,9 +21,9 @@ type vernac_toplevel =
   | VernacControl of vernac_control
 
 module Toplevel_ : sig
-  val vernac_toplevel : vernac_toplevel CAst.t Gram.entry
+  val vernac_toplevel : vernac_toplevel CAst.t Entry.t
 end = struct
-  let gec_vernac s = Gram.entry_create ("toplevel:" ^ s)
+  let gec_vernac s = Entry.create ("toplevel:" ^ s)
   let vernac_toplevel = gec_vernac "vernac_toplevel"
 end
 
@@ -49,6 +49,6 @@ END
 
 {
 
-let parse_toplevel pa = Pcoq.Gram.entry_parse vernac_toplevel pa
+let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa
 
 }
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c1bbb20d5..c914bbecf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -121,7 +121,7 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
   let in_echo = if echo then Some (open_utf8_file_in file) else None in
   let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in
 
-  let in_pa   = Pcoq.Gram.parsable ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
+  let in_pa   = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in
   let rstate  = ref state in
   (* For beautify, list of parsed sids *)
   let rids    = ref [] in
@@ -159,12 +159,12 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
       rstate := state;
     done;
     input_cleanup ();
-    !rstate, !rids, Pcoq.Gram.comment_state in_pa
+    !rstate, !rids, Pcoq.Parsable.comment_state in_pa
   with any ->   (* whatever the exception *)
     let (e, info) = CErrors.push any in
     input_cleanup ();
     match e with
-    | Stm.End_of_input -> !rstate, !rids, Pcoq.Gram.comment_state in_pa
+    | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa
     | reraise -> iraise (e, info)
 
 let process_expr ~state loc_ast =
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 48f225f97..3281b75aa 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -240,14 +240,14 @@ type (_, _) entry =
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
 (* This computes the name of the level where to add a new rule *)
-let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option =
+let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option =
   fun forpat level -> match forpat with
   | ForConstr ->
     if level = 200 then Constr.binder_constr, None
     else Constr.operconstr, Some level
   | ForPattern -> Constr.pattern, Some level
 
-let target_entry : type s. s target -> s Gram.entry = function
+let target_entry : type s. s target -> s Entry.t = function
 | ForConstr -> Constr.operconstr
 | ForPattern -> Constr.pattern
 
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index 31aa1a989..a5ee036db 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -21,7 +21,7 @@ type 's grammar_prod_item =
       ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
-  Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
+  Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option ->
     vernac_expr grammar_prod_item list -> unit
 
 val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index cccdbfc91..dacef6e21 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -22,7 +22,7 @@ open Pvernac.Vernac_
 
 let thm_token = G_vernac.thm_token
 
-let hint = Gram.entry_create "hint"
+let hint = Entry.create "hint"
 
 let warn_deprecated_focus =
   CWarnings.create ~name:"deprecated-focus" ~category:"deprecated"
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index e9d6ed9f6..a35a1998d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -37,18 +37,18 @@ let _ = List.iter CLexer.add_keyword vernac_kw
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
-let query_command = Gram.entry_create "vernac:query_command"
-
-let subprf = Gram.entry_create "vernac:subprf"
-
-let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
-let thm_token = Gram.entry_create "vernac:thm_token"
-let def_body = Gram.entry_create "vernac:def_body"
-let decl_notation = Gram.entry_create "vernac:decl_notation"
-let record_field = Gram.entry_create "vernac:record_field"
-let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion"
-let instance_name = Gram.entry_create "vernac:instance_name"
-let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
+let query_command = Entry.create "vernac:query_command"
+
+let subprf = Entry.create "vernac:subprf"
+
+let class_rawexpr = Entry.create "vernac:class_rawexpr"
+let thm_token = Entry.create "vernac:thm_token"
+let def_body = Entry.create "vernac:def_body"
+let decl_notation = Entry.create "vernac:decl_notation"
+let record_field = Entry.create "vernac:record_field"
+let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
+let instance_name = Entry.create "vernac:instance_name"
+let section_subset_expr = Entry.create "vernac:section_subset_expr"
 
 let make_bullet s =
   let open Proof_bullet in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 240147c8d..33e6229b2 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -49,7 +49,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.Gram.entry_print ft e in
+  let () = Pcoq.Entry.print ft e in
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index f8b085f3e..74e53bef1 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -178,7 +178,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.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us)))
+let using_from_string us = Pcoq.Entry.parse G_vernac.section_subset_expr (Pcoq.Parsable.make (Stream.of_string us))
 
 let _ =
   Goptions.declare_stringopt_option
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index bac882381..b2fa8ec99 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -10,13 +10,11 @@
 
 open Pcoq
 
-let uncurry f (x,y) = f x y
-
 let uvernac = create_universe "vernac"
 
 module Vernac_ =
   struct
-    let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
+    let gec_vernac s = Entry.create ("vernac:" ^ s)
 
     (* The different kinds of vernacular commands *)
     let gallina = gec_vernac "gallina"
@@ -28,22 +26,23 @@ module Vernac_ =
     let red_expr = new_entry utactic "red_expr"
     let hint_info = gec_vernac "hint_info"
     (* Main vernac entry *)
-    let main_entry = Gram.entry_create "vernac"
+    let main_entry = Entry.create "vernac"
     let noedit_mode = gec_vernac "noedit_command"
 
     let () =
-      let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in
-      let act_eoi = Gram.action (fun _ loc -> None) in
+      let open Extend in
+      let act_vernac v loc = Some (loc, v) in
+      let act_eoi _ loc = None in
       let rule = [
-        ([ Symbols.stoken Tok.EOI ], act_eoi);
-        ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
+        Rule (Next (Stop, Atoken Tok.EOI), act_eoi);
+        Rule (Next (Stop, Aentry vernac_control), act_vernac);
       ] in
-      uncurry (Gram.extend main_entry) (None, [None, None, rule])
+      Pcoq.grammar_extend main_entry None (None, [None, None, rule])
 
     let command_entry_ref = ref noedit_mode
     let command_entry =
       Gram.Entry.of_parser "command_entry"
-        (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
+        (fun strm -> Gram.Entry.parse_token !command_entry_ref strm)
 
   end
 
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 2993a1661..b2f8f7146 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -16,21 +16,21 @@ val uvernac : gram_universe
 
 module Vernac_ :
   sig
-    val gallina : vernac_expr Gram.entry
-    val gallina_ext : vernac_expr Gram.entry
-    val command : vernac_expr Gram.entry
-    val syntax : vernac_expr Gram.entry
-    val vernac_control : vernac_control Gram.entry
-    val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
-    val noedit_mode : vernac_expr Gram.entry
-    val command_entry : vernac_expr Gram.entry
-    val red_expr : raw_red_expr Gram.entry
-    val hint_info : Hints.hint_info_expr Gram.entry
+    val gallina : vernac_expr Entry.t
+    val gallina_ext : vernac_expr Entry.t
+    val command : vernac_expr Entry.t
+    val syntax : vernac_expr Entry.t
+    val vernac_control : vernac_control Entry.t
+    val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
+    val noedit_mode : vernac_expr Entry.t
+    val command_entry : vernac_expr Entry.t
+    val red_expr : raw_red_expr Entry.t
+    val hint_info : Hints.hint_info_expr Entry.t
   end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : (Loc.t * vernac_control) option Gram.entry
+val main_entry : (Loc.t * vernac_control) option Entry.t
 
 (** Handling of the proof mode entry *)
-val get_command_entry : unit -> vernac_expr Gram.entry
-val set_command_entry : vernac_expr Gram.entry -> unit
+val get_command_entry : unit -> vernac_expr Entry.t
+val set_command_entry : vernac_expr Entry.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 27f2a740e..b6bc76a2e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2040,7 +2040,7 @@ let vernac_load interp fname =
     interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
-    match Pcoq.Gram.entry_parse Pvernac.main_entry po with
+    match Pcoq.Entry.parse Pvernac.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
   let fname =
@@ -2049,7 +2049,7 @@ let vernac_load interp fname =
   let input =
     let longfname = Loadpath.locate_file fname in
     let in_chan = open_utf8_file_in longfname in
-    Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
+    Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in
   begin
     try while true do interp (snd (parse_sentence input)) done
     with End_of_input -> ()