diff options
| -rw-r--r-- | doc/RefMan-oth.tex | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex index 9017bbd15..57acfa3c4 100644 --- a/doc/RefMan-oth.tex +++ b/doc/RefMan-oth.tex @@ -616,18 +616,18 @@ skipped. They are not printed and the user must not give them. To show what are the implicit arguments associated to a declaration {\qualid}, use \texttt{Print \qualid}. You can change the implicit arguments of a specific declaration by using the command -\texttt{Implicits} (see section \ref{Implicits}). You can explicitely +\texttt{Implicits} (see section \ref{Implicits}). You can explicitly give an argument which otherwise should be implicit by using the symbol \verb=!= (see section \ref{Implicits-explicitation}). To set the implicit argument mode off, use {\tt Unset Implicit Arguments.} -\begin{Variants} -\item {\tt Implicit Arguments On.}\comindex{Implicit Arguments On}\\ -This is a deprecated equivalent to {\tt Set Implicit Arguments.} -\item {\tt Implicit Arguments Off.}\comindex{Implicit Arguments Off}\\ -This is a deprecated equivalent to {\tt Unset Implicit Arguments.} -\end{Variants} +% \begin{Variants} +% \item {\tt Implicit Arguments On.}\comindex{Implicit Arguments On}\\ +% This is a deprecated equivalent to {\tt Set Implicit Arguments.} +% \item {\tt Implicit Arguments Off.}\comindex{Implicit Arguments Off}\\ +% This is a deprecated equivalent to {\tt Unset Implicit Arguments.} +% \end{Variants} \SeeAlso section \ref{Auto-implicit} |