author lcp Tue, 28 Mar 1995 10:24:45 +0200 changeset 975 6c280d1dac35 parent 974 68d58134fad6 child 976 14b55f7fbf15
Corrected faulty reference to Hindley-Milner type inference
 doc-src/Logics/CTT.tex file | annotate | diff | comparison | revisions
--- 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$]