summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/CTT.tex

changeset 975 | 6c280d1dac35 |

parent 333 | 2ca08f62df33 |

child 3096 | ccc2c92bb232 |

--- 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$]