8 files changed, 40 insertions, 41 deletions
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