Introduce a Pcoq.Entry module for functions that ought to be exported.

We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.

Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.

27 files changed, 230 insertions, 198 deletions

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 93d65df2f..6726603e6 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -88,11 +88,10 @@ module type S =
   type action = Gramext.g_action
   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
 
@@ -107,7 +106,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
 
   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
@@ -132,7 +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
+
+  let create = G.Entry.create
+  let parse = G.entry_parse
+  let print = G.Entry.print
 
 end
 
@@ -347,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]);
@@ -364,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
 
@@ -385,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
@@ -402,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
@@ -414,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
 
@@ -453,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
@@ -464,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
 
@@ -591,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 ae4f5cab6..029c43713 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -24,21 +24,34 @@ module Gram : sig
   include Grammar.S with type te = Tok.t
 
   type 'a entry = 'a Entry.e
+  [@@ocaml.deprecated "Use [Pcoq.Entry.t]"]
 
-  type coq_parsable
+  [@@@ocaml.warning "-3"]
 
-  val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
   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
 
+  [@@@ocaml.warning "+3"]
+
 end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
 
+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
+
+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:
 
    - dynamic rules declared at the evaluation of Coq files (using
@@ -120,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
@@ -209,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
@@ -225,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,
@@ -255,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 3a01ce6df..2c60abfe3 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 aea66a07a..b2fa8ec99 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -14,7 +14,7 @@ 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"
@@ -26,7 +26,7 @@ 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 () =
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 5fda1a0da..8064856a6 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 -> ()