Merge branch 'v8.5'

4 files changed, 45 insertions, 0 deletions

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.
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..7e2610c7d7
--- /dev/null
+++ b/test-suite/output/ltac.v
@@ -0,0 +1,17 @@
+(* 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.
+
+(* 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
+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.