More complete printing of Ltac location, akin to the term-dedicated Locate command.

2 files changed, 22 insertions, 0 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 80beae8ae3..42f3089559 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -349,6 +349,27 @@ let print_located_qualid ref =
 	   else mt ()) ++
           display_alias o)) l
 
+let print_located_tactic r =
+  let (loc,qid) = qualid_of_reference r in
+  let all = Nametab.locate_extended_all_tactic qid in
+  let ans = List.map (fun qid -> (qid, Nametab.shortest_qualid_of_tactic qid)) all in
+  match ans with
+  | [] ->
+    str "No Ltac definition is referred to by " ++ pr_qualid qid
+  | _ ->
+    let print (obj, oqid) =
+      let path = Nametab.path_of_tactic obj in
+      let msg = str "Ltac" ++ spc () ++ pr_path path in
+      let short =
+        if not (qualid_eq oqid qid) then
+          spc() ++ str "(shorter name to refer to it in current context is "
+          ++ pr_qualid oqid ++ str")"
+        else mt ()
+      in
+      hov 2 (msg ++ short)
+    in
+    prlist_with_sep fnl print ans
+
 (******************************************)
 (**** Printing declarations and judgments *)
 (****  Gallina layer                  *****)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 0cbb7a86c4..bc0ce17186 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -54,6 +54,7 @@ val inspect : int -> std_ppcmds
 
 (** Locate *)
 val print_located_qualid : reference -> std_ppcmds
+val print_located_tactic : reference -> std_ppcmds
 
 type object_pr = {
   print_inductive           : mutual_inductive -> std_ppcmds;