Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" -> "constr"

Reviewed-by: herbelin
Ack-by: Zimmi48

7 files changed, 25 insertions, 27 deletions

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index a1094e39a4..bbc4df7dde 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -151,7 +151,7 @@ let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Gena
   Genarg.create_arg "function_rec_definition_loc"
 
 let function_rec_definition_loc =
-  Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+  Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
 
 }
 
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d88cda177e..be0d71ad46 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -48,14 +48,14 @@ let reference_to_id qid =
     CErrors.user_err ?loc:qid.CAst.loc
       (str "This expression should be a simple identifier.")
 
-let tactic_mode = Entry.create "vernac:tactic_command"
+let tactic_mode = Entry.create "tactic_command"
 
 let new_entry name =
   let e = Entry.create name in
   e
 
-let toplevel_selector = new_entry "vernac:toplevel_selector"
-let tacdef_body = new_entry "tactic:tacdef_body"
+let toplevel_selector = new_entry "toplevel_selector"
+let tacdef_body = new_entry "tacdef_body"
 
 (* Registers [tactic_mode] as a parser for proof editing *)
 let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index a6673699af..fc24475a62 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -56,7 +56,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 Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac)
+let withtac = Pcoq.create_generic_entry2 "withtac" (Genarg.rawwit wit_withtac)
 
 }
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 09cdc997ab..8331927cda 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -219,7 +219,7 @@ type binders_argtype = local_binder_expr list
 let wit_binders =
  (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
 
-let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
+let binders = Pcoq.create_generic_entry2 "binders" (Genarg.rawwit wit_binders)
 
 let () =
   let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 5b5ee64a56..b7b54143df 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -11,39 +11,37 @@
 open Pcoq
 
 (* Main entry for extensions *)
-let simple_tactic = Entry.create "tactic:simple_tactic"
-
-let make_gen_entry _ name = Entry.create ("tactic:" ^ name)
+let simple_tactic = Entry.create "simple_tactic"
 
 (* Typically for tactic user extensions *)
 let open_constr =
-  make_gen_entry utactic "open_constr"
+  Entry.create "open_constr"
 let constr_with_bindings =
-  make_gen_entry utactic "constr_with_bindings"
+  Entry.create "constr_with_bindings"
 let bindings =
-  make_gen_entry utactic "bindings"
+  Entry.create "bindings"
 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 constr_may_eval = Entry.create "constr_may_eval"
+let constr_eval = Entry.create "constr_eval"
 let uconstr =
-  make_gen_entry utactic "uconstr"
+  Entry.create "uconstr"
 let quantified_hypothesis =
-  make_gen_entry utactic "quantified_hypothesis"
-let destruction_arg = make_gen_entry utactic "destruction_arg"
-let int_or_var = make_gen_entry utactic "int_or_var"
+  Entry.create "quantified_hypothesis"
+let destruction_arg = Entry.create "destruction_arg"
+let int_or_var = Entry.create "int_or_var"
 let simple_intropattern =
-  make_gen_entry utactic "simple_intropattern"
-let in_clause = make_gen_entry utactic "in_clause"
+  Entry.create "simple_intropattern"
+let in_clause = Entry.create "in_clause"
 let clause_dft_concl =
-  make_gen_entry utactic "clause"
+  Entry.create "clause"
 
 
 (* Main entries for ltac *)
-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"
+let tactic_arg = Entry.create "tactic_arg"
+let tactic_expr = Entry.create "tactic_expr"
+let binder_tactic = Entry.create "binder_tactic"
 
-let tactic = make_gen_entry utactic "tactic"
+let tactic = Entry.create "tactic"
 
 (* Main entry for quotations *)
 let tactic_eoi = eoi_entry tactic
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fcd60ea250..f0ca813b08 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -869,7 +869,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
     let () = Pcoq.register_grammar wit e in
     e
   | Vernacextend.Arg_rules rules ->
-    let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
+    let e = Pcoq.create_generic_entry2 name (Genarg.rawwit wit) in
     let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in
     e
   in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index b32b58062a..89e0c9fcbe 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -403,7 +403,7 @@ END
 let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt ()
 
 let wit_ssrmmod = add_genarg "ssrmmod" (fun env sigma -> pr_mmod)
-let ssrmmod = Pcoq.create_generic_entry Pcoq.utactic "ssrmmod" (Genarg.rawwit wit_ssrmmod);;
+let ssrmmod = Pcoq.create_generic_entry2 "ssrmmod" (Genarg.rawwit wit_ssrmmod);;
 
 }