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

5 files changed, 26 insertions, 9 deletions

diff --git a/library/nametab.ml b/library/nametab.ml
index 1a30e80d1..4a61a9540 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -427,6 +427,8 @@ let locate_all qid =
 
 let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab
 
+let locate_extended_all_tactic qid = KnTab.find_prefixes qid !the_tactictab
+
 (* Derived functions *)
 
 let locate_constant qid =
diff --git a/library/nametab.mli b/library/nametab.mli
index d9038c774..ed4200456 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -111,6 +111,7 @@ val global_inductive : reference -> inductive
 
 val locate_all : qualid -> global_reference list
 val locate_extended_all : qualid -> extended_global_reference list
+val locate_extended_all_tactic : qualid -> ltac_constant list
 
 (** Mapping a full path to a global reference *)
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 80beae8ae..42f308955 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 0cbb7a86c..bc0ce1718 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;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 074d260c7..737d1c523 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -408,14 +408,6 @@ let print_located_module r =
     else
       msg_error (str "No module is referred to by name" ++ spc () ++ pr_qualid qid)
 
-let print_located_tactic r =
-  let (loc,qid) = qualid_of_reference r in
-  try
-    let path = Nametab.path_of_tactic (Nametab.locate_tactic qid) in
-    msg_notice (str "Ltac " ++ pr_path path)
-  with Not_found ->
-    msg_error (str "No Ltac definition is referred to by " ++ pr_qualid qid)
-
 let smart_global r =
   let gr = Smartlocate.smart_global r in
     Dumpglob.add_glob (Constrarg.loc_of_or_by_notation loc_of_reference r) gr;
@@ -1547,7 +1539,7 @@ let vernac_locate = function
           (Constrextern.without_symbols pr_lglob_constr) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> print_located_module qid
-  | LocateTactic qid -> print_located_tactic qid
+  | LocateTactic qid -> msg_notice (print_located_tactic qid)
   | LocateFile f -> msg_notice (locate_file f)
 
 let vernac_register id r =