diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-01 14:35:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-07-01 14:35:27 +0200 |
| commit | 2e8fb20e04da220cba68443a779c7ef6b08af9e5 (patch) | |
| tree | 0047aa2e7c4dfe5e803117a4d610d3b56b05e066 /doc/refman/RefMan-sch.tex | |
| parent | ff9f946343298e0d980e686654e7facfc28dc7d7 (diff) | |
Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"
Diffstat (limited to 'doc/refman/RefMan-sch.tex')
| -rw-r--r-- | doc/refman/RefMan-sch.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 707ee8240..c80e3ceeb 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -123,7 +123,7 @@ The type of {\tt even\_odd} shares the same premises but the conclusion is {\tt (n:nat)(even n)->(Q n)}. \subsection{Automatic declaration of schemes} -\comindex{Set Equality Schemes} +\comindex{Set Boolean Equality Schemes} \comindex{Set Elimination Schemes} It is possible to deactivate the automatic declaration of the induction @@ -133,7 +133,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 Schemes} +(see the second variant of {\tt Scheme}) with the {\tt Set Boolean 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. |