aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/coretactics.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/coretactics.ml4')
-rw-r--r--plugins/ltac/coretactics.ml48
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 07b8746fb..50013f558 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -17,7 +17,7 @@ open Stdarg
open Extraargs
open Names
-DECLARE PLUGIN "coretactics"
+DECLARE PLUGIN "ltac_plugin"
(** Basic tactics *)
@@ -324,11 +324,11 @@ let initial_atomic () =
"fresh", TacArg(Loc.tag @@ TacFreshId [])
]
-let () = Mltop.declare_cache_obj initial_atomic "coretactics"
+let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin"
(* First-class Ltac access to primitive blocks *)
-let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; }
+let initial_name s = { mltac_plugin = "ltac_plugin"; mltac_tactic = s; }
let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
let register_list_tactical name f =
@@ -356,4 +356,4 @@ let initial_tacticals () =
"solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
]
-let () = Mltop.declare_cache_obj initial_tacticals "coretactics"
+let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"