From eea3ff52329a8ac6e78cddc1121efb4e874a6961 Mon Sep 17 00:00:00 2001
From: vsiles
Date: Tue, 27 Apr 2010 14:33:20 +0000
Subject:  small detail about Scheme Equality

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12966 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 0b2c930b56..139f80cf3c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4154,7 +4154,8 @@ 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
-  decidability of the usual equality.
+  decidability of the usual equality. If \ident$_i$ involves
+  some other inductive types, their equality has to be defined first.
 
 \item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\
   with\\
-- 
cgit v1.2.3