Adding the Print Ltac Signatures command.

4 files changed, 40 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index cc7e6b53bf..12dea9a306 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1116,6 +1116,8 @@ Defined {\ltac} functions can be displayed using the command
 {\tt Print Ltac {\qualid}.}
 \end{quote}
 
+The command {\tt Print Ltac Signatures\comindex{Print Ltac Signatures}} displays a list of all user-defined tactics, with their arguments.
+
 \section{Debugging {\ltac} tactics}
 
 \subsection[Info trace]{Info trace\comindex{Info}\optindex{Info Level}}
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 308b6415d7..3579fc10f6 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -445,3 +445,7 @@ VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
     Tacentries.register_ltac (Locality.make_module_locality lc) l
   ]
 END
+
+VERNAC COMMAND EXTEND VernacPrintLtacs CLASSIFIED AS QUERY
+| [ "Print" "Ltac" "Signatures" ] -> [ Tacentries.print_ltacs () ]
+END
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 1d9e7b34e8..f00adecf2a 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -480,3 +480,32 @@ let register_ltac local tacl =
     Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
   in
   List.iter iter defs
+
+(** Queries *)
+
+let print_ltacs () =
+  let entries = KNmap.bindings (Tacenv.ltac_entries ()) in
+  let sort (kn1, _) (kn2, _) = KerName.compare kn1 kn2 in
+  let entries = List.sort sort entries in
+  let map (kn, entry) =
+    let qid =
+      try Some (Nametab.shortest_qualid_of_tactic kn)
+      with Not_found -> None
+    in
+    match qid with
+    | None -> None
+    | Some qid -> Some (qid, entry.Tacenv.tac_body)
+  in
+  let entries = List.map_filter map entries in
+  let pr_entry (qid, body) =
+    let (l, t) = match body with
+    | Tacexpr.TacFun (l, t) -> (l, t)
+    | _ -> ([], body)
+    in
+    let pr_ltac_fun_arg = function
+    | None -> spc () ++ str "_"
+    | Some id -> spc () ++ pr_id id
+    in
+    hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
+  in
+  Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli
index 402cb2fc96..27df819ee6 100644
--- a/ltac/tacentries.mli
+++ b/ltac/tacentries.mli
@@ -57,3 +57,8 @@ val create_ltac_quotation : string ->
 (** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
     Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
     generates an argument using [f] on the entry parsed by [e]. *)
+
+(** {5 Queries} *)
+
+val print_ltacs : unit -> unit
+(** Display the list of ltac definitions currently available. *)