diff options
| author | Enrico Tassi | 2019-05-29 13:08:25 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-29 13:08:25 +0200 |
| commit | d62215a4c06680d2052238544b9e31422f512eaf (patch) | |
| tree | fbf204c413eaf95d1c07c76d61cceb830ae6d2d4 /doc/changelog | |
| parent | 09514118c386420650847ba74c7f985bb0a05776 (diff) | |
| parent | 44f87dae748f8c84b7c9290b00c4d76197e5497a (diff) | |
Merge PR #10049: [elaboration] Bidirectionality hints
Ack-by: RalfJung
Reviewed-by: SkySkimmer
Reviewed-by: gares
Ack-by: maximedenes
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/02-specification-language/10049-bidi-app.rst | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst new file mode 100644 index 0000000000..79678c5242 --- /dev/null +++ b/doc/changelog/02-specification-language/10049-bidi-app.rst @@ -0,0 +1,6 @@ +- New 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`. + `#10049 <https://github.com/coq/coq/pull/10049>`_, by Maxime Dénès with + help from Enrico Tassi |