From 0bc5690260483be052f86b73ee3a73fe62a5110c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin 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