Ltac uses the new generic locatable API.

3 files changed, 33 insertions, 0 deletions

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. *)