From 88cfa53f8e893c92798fab97f8886b4bb3f84a3b Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 17 Apr 2004 09:30:11 +0000 Subject: Typos, ajout Set Printing All git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8548 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/RefMan-syn.tex | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'doc/RefMan-syn.tex') diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex index 3fffcdf21..e15935ece 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}} -- cgit v1.2.3