blob: 024795f5dad672a13c12c8d668c0630444e43766 (
plain)
1
2
3
4
5
6
7
|
- **Added:**
Annotation in `Arguments` for bidirectionality hints: it is now possible
to tell type inference to use type information from the context once the `n`
first arguments of an application are known. The syntax is:
`Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)`
(`#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with
help from Enrico Tassi).
|
