| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-28 | [elaboration] Bidirectionality hints | Maxime Dénès | |
| This feature makes it possible to tell type inference to type applications of a global `foo` using typing information from the context once the `n` first arguments are known. The syntax is: `Arguments foo x y | z`. Closes #7910 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |