diff -r 68d58134fad6 -r 6c280d1dac35 doc-src/Logics/CTT.tex
--- 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$]