1 files changed, 31 insertions, 15 deletions

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 84c0a99b..09a98bc8 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -26,6 +26,8 @@ let interp_alias key =
   try KNmap.find key !alias_map
   with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
 
+let check_alias key = KNmap.mem key !alias_map
+
 (** ML tactic extensions (TacML) *)
 
 type ml_tactic =
@@ -43,7 +45,7 @@ end
 module MLTacMap = Map.Make(MLName)
 
 let pr_tacname t =
-  t.mltac_plugin ^ "::" ^ t.mltac_tactic
+  str t.mltac_plugin ++ str "::" ++ str t.mltac_tactic
 
 let tac_tab = ref MLTacMap.empty
 
@@ -52,9 +54,9 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
     if MLTacMap.mem s !tac_tab then
       if overwrite then
         let () = tac_tab := MLTacMap.remove s !tac_tab in
-        msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s))
+        msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s)
       else
-        Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ "."))
+        Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
   in
   tac_tab := MLTacMap.add s t !tac_tab
 
@@ -63,7 +65,7 @@ let interp_ml_tactic s =
     MLTacMap.find s !tac_tab
   with Not_found ->
     Errors.errorlabstrm ""
-      (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
+      (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
 
 (***************************************************************************)
 (* Tactic registration *)
@@ -73,34 +75,48 @@ let interp_ml_tactic s =
 open Nametab
 open Libobject
 
+type ltac_entry = {
+  tac_for_ml : bool;
+  tac_body : glob_tactic_expr;
+  tac_redef : ModPath.t list;
+}
+
 let mactab =
-  Summary.ref (KNmap.empty : (bool * glob_tactic_expr) KNmap.t)
+  Summary.ref (KNmap.empty : ltac_entry KNmap.t)
     ~name:"tactic-definition"
 
-let interp_ltac r = snd (KNmap.find r !mactab)
+let ltac_entries () = !mactab
+
+let interp_ltac r = (KNmap.find r !mactab).tac_body
+
+let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml
 
-let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab)
+let add kn b t =
+  let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in
+  mactab := KNmap.add kn entry !mactab
 
-(* Declaration of the TAC-DEFINITION object *)
-let add (kn,td) = mactab := KNmap.add kn td !mactab
+let replace kn path t =
+  let (path, _, _) = KerName.repr path in
+  let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
+  mactab := KNmap.modify kn entry !mactab
 
 let load_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
   let () = if not local then Nametab.push_tactic (Until i) sp kn in
-  add (kn, (b,t))
-| Some kn -> add (kn, (b,t))
+  add kn b t
+| Some kn0 -> replace kn0 kn t
 
 let open_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
   let () = if not local then Nametab.push_tactic (Exactly i) sp kn in
-  add (kn, (b,t))
-| Some kn -> add (kn, (b,t))
+  add kn b t
+| Some kn0 -> replace kn0 kn t
 
 let cache_md ((sp, kn), (local, id ,b, t)) = match id with
 | None ->
   let () = Nametab.push_tactic (Until 1) sp kn in
-  add (kn, (b,t))
-| Some kn -> add (kn, (b,t))
+  add kn b t
+| Some kn0 -> replace kn0 kn t
 
 let subst_kind subst id = match id with
 | None -> None