diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/CanonicalStructures.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex index a3372c2965..275e1c2d55 100644 --- a/doc/refman/CanonicalStructures.tex +++ b/doc/refman/CanonicalStructures.tex @@ -4,7 +4,7 @@ \label{CS-full} \index{Canonical Structures!presentation} -This chapter explains the basics of Canonical Structure and how thy can be used +\noindent This chapter explains the basics of Canonical Structure and how they can be used to overload notations and build a hierarchy of algebraic structures. The examples are taken from~\cite{CSwcu}. We invite the interested reader to refer to this paper for all the details that are omitted here for brevity. 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}} |