diff options
| author | Gaëtan Gilbert | 2019-12-23 23:08:45 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-01-06 22:48:39 +0100 |
| commit | 0d73faf60f89c62e4ecd6b28cb45b8a2c044859d (patch) | |
| tree | 06589b585379636fb83d4f44f5975d05e6eb96ff | |
| parent | 15ec807cd201b49ed339d665c34c955a36b29745 (diff) | |
doc: mention limitation of bidi hints vs program
No example as I'm not familiar enough with Program to make one.
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 78428be18f..8d59e64cdb 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2547,3 +2547,8 @@ the context to help inferring the types of the remaining arguments. Arguments ex_intro _ _ & _ _. Check (ex_intro _ true _ : exists n : nat, n > 0). + +Coq will attempt to produce a term which uses the arguments you +provided, but in some cases involving Program mode the arguments after +the bidirectionality starts may be replaced by convertible but +syntactically different terms. |