From 0bc5690260483be052f86b73ee3a73fe62a5110c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 3 Oct 2014 17:10:26 +0200
Subject: Fixing #3606 continued (doc of Scheme Boolean Equality Scheme).

---
 doc/refman/RefMan-sch.tex | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'doc/refman/RefMan-sch.tex')

diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex
index e28e4a443..7d00a4005 100644
--- a/doc/refman/RefMan-sch.tex
+++ b/doc/refman/RefMan-sch.tex
@@ -33,7 +33,7 @@ general principle of mutual induction for objects in type {\term$_i$}.
 
 \item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}}
 
-  Tries to generate a boolean equality and a proof of the
+  Tries to generate a Boolean equality and a proof of the
   decidability of the usual equality. If \ident$_i$ involves
   some other inductive types, their equality has to be defined first.
 
@@ -144,11 +144,13 @@ command {\tt Set Nonrecursive Elimination Schemes}. It can be
 deactivated again with {\tt Unset Nonrecursive Elimination Schemes}.
 \\
 
-You can also activate the automatic declaration of those boolean equalities
-(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
+You can also activate the automatic declaration of those Boolean equalities
+(see the second variant of {\tt Scheme})
+with respectively the commands {\tt Set Boolean Equality Schemes} and
+{\tt Set Decidable Equality Schemes}.
+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.
+a Boolean equality for them.
 
 \subsection{\tt Combined Scheme}
 \label{CombinedScheme}
-- 
cgit v1.2.3

