From 2e8fb20e04da220cba68443a779c7ef6b08af9e5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 1 Jul 2014 14:35:04 +0200 Subject: Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes" --- doc/refman/RefMan-sch.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/refman/RefMan-sch.tex') 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. -- cgit v1.2.3