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


From e9995f6e9f9523d4738d9ee494703b6f96bf995d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 14:36:29 +0200
Subject: Fixing untimely unexpected warning "Collision between bound
 variables" (#4317).

Collecting the bound variables is now done on the glob_constr, before
interpretation, so that only variables given explicitly by the user
are used for binding bound variables.
---
 test-suite/output/ltac.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 567e21edbe..9a60afe5f6 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -6,3 +6,12 @@ Fail let T := constr:((fun a b : nat => a+b) 1 1) in
     => pose ((fun x _ => y) 1 1)
   end.
 Abort.
+
+(* This should not raise a warning (see #4317) *)
+Goal True.
+assert (H:= eq_refl ((fun x => x) 1)).
+let HT := type of H in
+lazymatch goal with
+| H1 : HT |- _ => idtac "matched"
+end.
+Abort.
-- 
cgit v1.2.3


From cd9a2e9e59d87801790859ddd26d225d71be7f7c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Oct 2015 17:26:30 +0200
Subject: Fixing test-suite

---
 test-suite/output/ltac.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 9a60afe5f6..7e2610c7d7 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -12,6 +12,6 @@ Goal True.
 assert (H:= eq_refl ((fun x => x) 1)).
 let HT := type of H in
 lazymatch goal with
-| H1 : HT |- _ => idtac "matched"
+| H1 : HT |- _ => idtac
 end.
 Abort.
-- 
cgit v1.2.3


From 303694c6436b36b114f4919ad7cacc9c053d11a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 11 Oct 2015 19:06:26 +0200
Subject: Adding test for bug #4366.

---
 test-suite/bugs/closed/4366.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/4366.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
new file mode 100644
index 0000000000..6a5e9a4023
--- /dev/null
+++ b/test-suite/bugs/closed/4366.v
@@ -0,0 +1,15 @@
+Fixpoint stupid (n : nat) : unit :=
+match n with
+| 0 => tt
+| S n =>
+  let () := stupid n in
+  let () := stupid n in
+  tt
+end.
+
+Goal True.
+Proof.
+pose (v := stupid 24).
+Timeout 2 vm_compute in v.
+exact I.
+Qed.
-- 
cgit v1.2.3