Qualified ML tactic names. The plugin name is used to discriminate

potentially conflicting tactics names from different plugins.

3 files changed, 25 insertions, 11 deletions

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 073df91cfa..94a9d03dcd 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -31,25 +31,39 @@ let interp_alias key =
 type ml_tactic =
   typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
 
-let tac_tab = Hashtbl.create 17
+module MLName =
+struct
+  type t = ml_tactic_name
+  let compare tac1 tac2 =
+    let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in
+    if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin
+    else c
+end
+
+module MLTacMap = Map.Make(MLName)
+
+let pr_tacname t =
+  t.mltac_plugin ^ "::" ^ t.mltac_tactic
+
+let tac_tab = ref MLTacMap.empty
 
 let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
   let () =
-    if Hashtbl.mem tac_tab s then
+    if MLTacMap.mem s !tac_tab then
       if overwrite then
-        let () = Hashtbl.remove tac_tab s in
-        msg_warning (str ("Overwriting definition of tactic " ^ s))
+        let () = tac_tab := MLTacMap.remove s !tac_tab in
+        msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s))
       else
-        Errors.anomaly (str ("Cannot redeclare tactic " ^ s ^ "."))
+        Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ "."))
   in
-  Hashtbl.add tac_tab s t
+  tac_tab := MLTacMap.add s t !tac_tab
 
 let interp_ml_tactic s =
   try
-    Hashtbl.find tac_tab s
+    MLTacMap.find s !tac_tab
   with Not_found ->
     Errors.errorlabstrm ""
-      (str "The tactic " ++ str s ++ str " is not installed.")
+      (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
 
 let () =
   let assert_installed opn = let _ = interp_ml_tactic opn in () in
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index a7609ae215..4d64a5bb2b 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -45,8 +45,8 @@ type ml_tactic =
   typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
 (** Type of external tactics, used by [TacExtend]. *)
 
-val register_ml_tactic : ?overwrite:bool -> string -> ml_tactic -> unit
+val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit
 (** Register an external tactic. *)
 
-val interp_ml_tactic : string -> ml_tactic
+val interp_ml_tactic : ml_tactic_name -> ml_tactic
 (** Get the named tactic. Raises a user error if it does not exist. *)
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 22588fcf16..84e5782f8d 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -63,7 +63,7 @@ val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
 val dump_glob_red_expr : raw_red_expr -> unit
 
 (* Hooks *)
-val assert_tactic_installed_hook : (string -> unit) Hook.t
+val assert_tactic_installed_hook : (ml_tactic_name -> unit) Hook.t
 val interp_atomic_ltac_hook : (Id.t -> glob_tactic_expr) Hook.t
 val interp_ltac_hook : (KerName.t -> glob_tactic_expr) Hook.t
 val strict_check : bool ref