diff options
| -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. |