From ae5305a4837cce3c7fd61b92ce8110ac66ec2750 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 15:05:10 +0200
Subject: 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.
---
 test-suite/output/ltac.out |  2 ++
 test-suite/output/ltac.v   |  8 ++++++++
 test-suite/success/ltac.v  | 11 +++++++++++
 3 files changed, 21 insertions(+)
 create mode 100644 test-suite/output/ltac.out
 create mode 100644 test-suite/output/ltac.v

(limited to 'test-suite')

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