diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index c80532d23..f5bef115f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3626,7 +3626,7 @@ general principle of mutual induction for objects in type {\term$_i$}. \item {\tt Scheme Equality for \ident$_1$} - Tries to generate an boolean equality and a proof of the + Tries to generate a boolean equality and a proof of the decidability of the usual equality. \item {\tt Scheme Induction for \ident$_1$ Sort {\sort$_1$} \\ |