diff options
Diffstat (limited to 'doc/refman/Coercion.tex')
| -rw-r--r-- | doc/refman/Coercion.tex | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index 60b4b2241..e4aa69353 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -305,8 +305,7 @@ Print the list of valid coercion paths from {\class$_1$} to {\class$_2$}. \asection{Activating the Printing of Coercions} \asubsection{\tt Set Printing Coercions.} -\comindex{Set Printing Coercions} -\comindex{Unset Printing Coercions} +\optindex{Printing Coercions} This command forces all the coercions to be printed. Conversely, to skip the printing of coercions, use @@ -314,8 +313,7 @@ Conversely, to skip the printing of coercions, use By default, coercions are not printed. \asubsection{\tt Set Printing Coercion {\qualid}.} -\comindex{Set Printing Coercion} -\comindex{Unset Printing Coercion} +\optindex{Printing Coercion} This command forces coercion denoted by {\qualid} to be printed. To skip the printing of coercion {\qualid}, use @@ -378,8 +376,7 @@ imported or not. To recover the behavior of the versions of Coq prior to 8.3, use the following command: -\comindex{Set Automatic Coercions Import} -\comindex{Unset Automatic Coercions Import} +\optindex{Automatic Coercions Import} \begin{verbatim} Set Automatic Coercions Import. \end{verbatim} |