From 0d73faf60f89c62e4ecd6b28cb45b8a2c044859d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 23 Dec 2019 23:08:45 +0100
Subject: doc: mention limitation of bidi hints vs program

No example as I'm not familiar enough with Program to make one.
---
 doc/sphinx/language/gallina-extensions.rst | 5 +++++
 1 file changed, 5 insertions(+)

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.
-- 
cgit v1.2.3