diff options
Diffstat (limited to 'doc/RefMan-syn.tex')
| -rwxr-xr-x | doc/RefMan-syn.tex | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex index 3fffcdf218..e15935ece4 100755 --- a/doc/RefMan-syn.tex +++ b/doc/RefMan-syn.tex @@ -400,19 +400,21 @@ where "n + m" := (plus n m). \end{coq_example*} \subsection{Displaying informations about notations -\comindex{Set Printing Notation} -\comindex{Unset Printing Notation}} +\comindex{Set Printing Notations} +\comindex{Unset Printing Notations}} To deactivate the printing of all notations, use the command \begin{quote} -\tt Unset Printing Notation. +\tt Unset Printing Notations. \end{quote} To reactivate it, use the command \begin{quote} -\tt Set Printing Notation. +\tt Set Printing Notations. \end{quote} The default is to use notations for printing terms wherever possible. +\SeeAlso {\tt Set Printing All} in section \ref{SetPrintingAll}. + \subsection{Locating notations \comindex{Locate} \label{LocateSymbol}} |