Granting wish #4048: Locate Ltac prints the source of redefined Ltac.

3 files changed, 53 insertions, 13 deletions

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 08e8bc011..09a98bc8c 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -75,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
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 9410ccb38..2df6bb04a 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -44,6 +44,19 @@ val interp_ltac : KerName.t -> glob_tactic_expr
 (** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *)
 
 val is_ltac_for_ml_tactic : KerName.t -> bool
+(** Whether the tactic is defined from ML-side *)
+
+type ltac_entry = {
+  tac_for_ml : bool;
+  (** Whether the tactic is defined from ML-side *)
+  tac_body : glob_tactic_expr;
+  (** The current body of the tactic *)
+  tac_redef : ModPath.t list;
+  (** List of modules redefining the tactic in reverse chronological order *)
+}
+
+val ltac_entries : unit -> ltac_entry KNmap.t
+(** Low-level access to all Ltac entries currently defined. *)
 
 (** {5 ML tactic extensions} *)
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 5cc4c835b..d4c67b90f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -809,11 +809,24 @@ let pr_ltac_fun_arg = function
 let print_ltac id =
  try
   let kn = Nametab.locate_tactic id in
-  let l,t = split_ltac_fun (Tacenv.interp_ltac kn) in
+  let entries = Tacenv.ltac_entries () in
+  let tac = KNmap.find kn entries in
+  let filter mp =
+    try Some (Nametab.shortest_qualid_of_module mp)
+    with Not_found -> None
+  in
+  let mods = List.map_filter filter tac.Tacenv.tac_redef in
+  let redefined = match mods with
+  | [] -> mt ()
+  | mods ->
+    let redef = prlist_with_sep fnl pr_qualid mods in
+    fnl () ++ str "Redefined by:" ++ fnl () ++ redef
+  in
+  let l,t = split_ltac_fun tac.Tacenv.tac_body in
   hv 2 (
     hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
            prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
-    ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t)
+    ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
  with
   Not_found ->
    errorlabstrm "print_ltac"