summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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

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