--- a/doc-src/Logics/CTT.tex Mon Mar 27 18:29:23 1995 +0200
+++ b/doc-src/Logics/CTT.tex Tue Mar 28 10:24:45 1995 +0200
@@ -533,8 +533,8 @@
\item[\ttindexbold{typechk_tac} $thms$]
uses $thms$ with formation, introduction, and elimination rules to check
the typing of constructions. It is designed to solve goals of the form
-$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible. Thus it
-performs Hindley-Milner type inference. The tactic can also solve goals of
+$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it
+performs type inference. The tactic can also solve goals of
the form $A\;\rm type$.
\item[\ttindexbold{equal_tac} $thms$]