1 files changed, 17 insertions, 19 deletions
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