Adding a universe argument to Pcoq.create_generic_entry.

7 files changed, 9 insertions, 9 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 46c68ecc3a..57ae357dec 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -147,7 +147,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
      <:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
      <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
      <:str_item<
-      value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
+      value $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ $rawwit$ >>;
      <:str_item< do {
       Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]);
       Pptactic.declare_extra_genarg_pprule
@@ -170,7 +170,7 @@ let declare_vernac_argument loc s pr cl =
       value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) =
         Genarg.create_arg $se$ >>;
      <:str_item<
-      value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
+      value $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ $rawwit$ >>;
     <:str_item< do {
       Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]);
       Pptactic.declare_extra_genarg_pprule $wit$
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 52437e3867..e150578196 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -251,7 +251,7 @@ let create_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.ent
 
 let create_constr_entry s = create_entry uconstr s (rawwit wit_constr)
 
-let create_generic_entry s wit = create_entry utactic s wit
+let create_generic_entry = create_entry
 
 (* [make_gen_entry] builds entries extensible by giving its name (a string) *)
 (* For entries extensible only via the ML name, Gram.entry_create is enough *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7e0c89fd12..625f0370e6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -162,8 +162,8 @@ val uvernac : gram_universe
 
 val get_entry : gram_universe -> string -> typed_entry
 
-val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
-  'a Gram.entry
+val create_generic_entry : gram_universe -> string ->
+  ('a, rlevel) abstract_argument_type -> 'a Gram.entry
 
 module Prim :
   sig
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 2d096a1081..2afbaca2c8 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -95,7 +95,7 @@ let proof_mode : vernac_expr Gram.entry =
   Gram.entry_create "vernac:proof_command"
 (* Auxiliary grammar entry. *)
 let proof_instr : raw_proof_instr Gram.entry =
-  Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr)
+  Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr)
 
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 61ada5cc8c..dbcdeb83ad 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -149,7 +149,7 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar
   Genarg.create_arg "function_rec_definition_loc"
 
 let function_rec_definition_loc =
-  Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+  Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
 
 GEXTEND Gram
   GLOBAL: function_rec_definition_loc ;
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 8b012aa88e..0ce886373f 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -186,7 +186,7 @@ type binders_argtype = local_binder list
 let wit_binders =
  (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
 
-let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders)
+let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
 
 open Pcoq
 
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 32ccf21d2b..2a5676525a 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -34,7 +34,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a
 let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
   Genarg.create_arg "withtac"
 
-let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac)
+let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac)
 
 GEXTEND Gram
   GLOBAL: withtac;