aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2015-11-07 11:02:40 +0100
committerHugo Herbelin2015-11-07 11:06:57 +0100
commitbbef0e8702bf5e2dcad9bb4c47f92858d4eea9b4 (patch)
tree4bac150903763786f51e2755ab143f95dd762e98
parentc5d380548ef5597b77c7ab1fce252704deefeaf1 (diff)
Fixing documention of Add Printing Coercion.
-rw-r--r--doc/refman/Coercion.tex7
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index e4aa69353d..16006a6adf 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -312,12 +312,13 @@ Conversely, to skip the printing of coercions, use
{\tt Unset Printing Coercions}.
By default, coercions are not printed.
-\asubsection{\tt Set Printing Coercion {\qualid}.}
-\optindex{Printing Coercion}
+\asubsection{\tt Add Printing Coercion {\qualid}.}
+\comindex{Add Printing Coercion}
+\comindex{Remove Printing Coercion}
This command forces coercion denoted by {\qualid} to be printed.
To skip the printing of coercion {\qualid}, use
- {\tt Unset Printing Coercion {\qualid}}.
+ {\tt Remove Printing Coercion {\qualid}}.
By default, a coercion is never printed.
\asection{Classes as Records}