5 files changed, 49 insertions, 1 deletions
diff --git a/API/API.ml b/API/API.ml
index 46ad36d36..bf99d0feb 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -212,7 +212,7 @@ module Pputils = Pputils
 module Ppconstr = Ppconstr
 module Printer = Printer
 (* module Printmod *)
-(* module Prettyp *)
+module Prettyp = Prettyp
 module Ppvernac = Ppvernac
 
 (******************************************************************************)
diff --git a/API/API.mli b/API/API.mli
index e2cb70583..3bd047043 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5005,6 +5005,21 @@ sig
   val pr_transparent_state : Names.transparent_state -> Pp.t
 end
 
+module Prettyp :
+sig
+  type 'a locatable_info = {
+    locate : Libnames.qualid -> 'a option;
+    locate_all : Libnames.qualid -> 'a list;
+    shortest_qualid : 'a -> Libnames.qualid;
+    name : 'a -> Pp.t;
+    print : 'a -> Pp.t;
+    about : 'a -> Pp.t;
+  }
+
+  val register_locatable : string -> 'a locatable_info -> unit
+  val print_located_other : string -> Libnames.reference -> Pp.t
+end
+
 (************************************************************************)
 (* End of modules from printing/                                        *)
 (************************************************************************)
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 86c983bdd..d639dd0e1 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -482,6 +482,11 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
   [ Feedback.msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
 END
 
+VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
+| [ "Locate" "Ltac" reference(r) ] ->
+  [ Tacentries.print_located_tactic r ]
+END
+
 let pr_ltac_ref = Libnames.pr_reference
 
 let pr_tacdef_body tacdef_body =
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 8573da19f..bcd5b388a 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -506,6 +506,31 @@ let print_ltacs () =
   in
   Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
 
+let locatable_ltac = "Ltac"
+
+let () =
+  let open Prettyp in
+  let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
+  let locate_all = Tacenv.locate_extended_all_tactic in
+  let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
+  let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
+  let print kn =
+    let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
+    Tacintern.print_ltac qid
+  in
+  let about = name in
+  register_locatable locatable_ltac {
+    locate;
+    locate_all;
+    shortest_qualid;
+    name;
+    print;
+    about;
+  }
+
+let print_located_tactic qid =
+  Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
+
 (** Grammar *)
 
 let () =
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index aa8f4efe6..ab2c6b307 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -62,3 +62,6 @@ val create_ltac_quotation : string ->
 
 val print_ltacs : unit -> unit
 (** Display the list of ltac definitions currently available. *)
+
+val print_located_tactic : Libnames.reference -> unit
+(** Display the absolute name of a tactic. *)