From 649d3753749c036f085b1da8fb423d452afc05df Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 5 Jun 2016 20:57:49 +0200
Subject: Adding the Print Ltac Signature command.

---
 doc/refman/RefMan-ltac.tex | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/refman')

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}}
-- 
cgit v1.2.3