From 2e8fb20e04da220cba68443a779c7ef6b08af9e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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

