Merge branch 'v8.6'

6 files changed, 88 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v
new file mode 100644
index 000000000..806ffb771
--- /dev/null
+++ b/test-suite/bugs/closed/4132.v
@@ -0,0 +1,31 @@
+
+Require Import ZArith Omega.
+Open Scope Z_scope.
+
+(** bug 4132: omega was using "simpl" either on whole equations, or on
+   delimited but wrong spots. This was leading to unexpected reductions
+   when one atom (here [b]) is an evaluable reference instead of a variable. *)
+
+Lemma foo
+  (x y x' zxy zxy' z : Z)
+  (b := 5)
+  (Ry : - b <= y < b)
+  (Bx : x' <= b)
+  (H : - zxy' <= zxy)
+  (H' : zxy' <= x') : - b <= zxy.
+Proof.
+omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *)
+Qed.
+
+Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b.
+omega. (* Pierre L: according to a comment of bug report #4132,
+          this might have triggered "index out of bounds" in the past,
+          but I never managed to reproduce that in any version,
+          even before my fix. *)
+Qed.
+
+Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
+omega. (* Pierre L: according to a comment of bug report #4132,
+          this might have triggered "Failure(occurence 2)" in the past,
+          but I never managed to reproduce that. *)
+Qed.
diff --git a/test-suite/bugs/closed/5019.v b/test-suite/bugs/closed/5019.v
new file mode 100644
index 000000000..7c973f88b
--- /dev/null
+++ b/test-suite/bugs/closed/5019.v
@@ -0,0 +1,5 @@
+Require Import Coq.ZArith.ZArith.
+Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d.
+  clear; intros.
+  Timeout 1 zify. (* used to loop forever; should take < 0.01 s *)
+Admitted.
diff --git a/test-suite/bugs/closed/5255.v b/test-suite/bugs/closed/5255.v
new file mode 100644
index 000000000..5daaf9edb
--- /dev/null
+++ b/test-suite/bugs/closed/5255.v
@@ -0,0 +1,24 @@
+Section foo.
+  Context (x := 1).
+  Definition foo : x = 1 := eq_refl.
+End foo.
+
+Module Type Foo.
+  Context (x := 1).
+  Definition foo : x = 1 := eq_refl.
+End Foo.
+
+Set Universe Polymorphism.
+
+Inductive unit := tt.
+Inductive eq {A} (x y : A) : Type := eq_refl : eq x y.
+
+Section bar.
+  Context (x := tt).
+  Definition bar : eq x tt := eq_refl _ _.
+End bar.
+
+Module Type Bar.
+  Context (x := tt).
+  Definition bar : eq x tt := eq_refl _ _.
+End Bar.
diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v
new file mode 100644
index 000000000..390133162
--- /dev/null
+++ b/test-suite/bugs/closed/5486.v
@@ -0,0 +1,15 @@
+Axiom proof_admitted : False.
+Tactic Notation "admit" := abstract case proof_admitted.
+Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k :
+									 forall _ : T, Fm),
+    @eq Fm
+	(k
+	   match p return T with
+	   | pair p0 swap => fst p0
+	   end) f.
+  intros.
+  (* next statement failed in Bug 5486 *)
+  match goal with
+  | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ]
+    => pose (let (a, b) := d in e a b) as t0
+  end.
diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v
new file mode 100644
index 000000000..88f219be3
--- /dev/null
+++ b/test-suite/bugs/closed/5526.v
@@ -0,0 +1,3 @@
+Fail Notation "x === x" := (eq_refl x) (at level 10).
+Reserved Notation "x === x" (only printing, at level 10).
+Notation "x === x" := (eq_refl x) (only printing).
diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v
new file mode 100644
index 000000000..bb1222489
--- /dev/null
+++ b/test-suite/bugs/closed/5550.v
@@ -0,0 +1,10 @@
+Section foo.
+
+  Variable bar : Prop.
+  Variable H : bar.
+
+  Goal bar.
+    typeclasses eauto with foobar.
+  Qed.
+
+End foo.