Refining 0c320e79ba30 in fixing interpretation of constr under binders

which was broken after it became possible to have binding names
themselves bound to ltac variables (2fcc458af16b).

Interpretation was corrected, but error message was damaged.

3 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
new file mode 100644
index 0000000000..d003c70df9
--- /dev/null
+++ b/test-suite/output/ltac.out
@@ -0,0 +1,2 @@
+The command has indeed failed with message:
+Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
new file mode 100644
index 0000000000..567e21edbe
--- /dev/null
+++ b/test-suite/output/ltac.v
@@ -0,0 +1,8 @@
+(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
+Goal True.
+Fail let T := constr:((fun a b : nat => a+b) 1 1) in
+  lazymatch T with
+  | (fun x z => ?y) 1 1
+    => pose ((fun x _ => y) 1 1)
+  end.
+Abort.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index f9df021dc2..6c4d4ae98f 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -306,3 +306,14 @@ let x := ipattern:y in assert (forall x y, x = y + 0).
 intro.
 destruct y. (* Check that the name is y here *)
 Abort.
+
+(* An example suggested by Jason (see #4317) showing the intended semantics *)
+(* Order of binders is reverted because y is just told to depend on x *)
+
+Goal 1=1.
+let T := constr:(fun a b : nat => a) in
+  lazymatch T with
+  | (fun x z => ?y) => pose ((fun x x => y) 2 1)
+  end.
+exact (eq_refl n).
+Qed.