diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 4edf1a41d1..4d5cdbb81c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4162,7 +4162,7 @@ general principle of mutual induction for objects in type {\term$_i$}. \SeeAlso Section~\ref{Scheme-examples} \subsection{Automatic declaration of schemes} -\comindex{Set Equality Scheme} +\comindex{Set Equality Schemes} \comindex{Set Elimination Schemes} It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the @@ -4171,7 +4171,7 @@ reactivated at any time with {\tt Set Elimination Schemes}. \\ You can also activate the automatic declaration of those boolean equalities -(see the second variant of {\tt Scheme}) with the {\tt Set Equality Scheme} +(see the second variant of {\tt Scheme}) with the {\tt Set Equality Schemes} command. However you have to be careful with this option since \Coq~ may now reject well-defined inductive types because it cannot compute a boolean equality for them. |