diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 3 |
1 files changed, 2 insertions, 1 deletions
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\\ |