5 files changed, 41 insertions, 4 deletions
diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/closed/3819.v
index 7105a65877..355d23a58b 100644
--- a/test-suite/bugs/opened/3819.v
+++ b/test-suite/bugs/closed/3819.v
@@ -1,5 +1,3 @@
-Set Universe Polymorphism.
-
 Record Op := { t : Type ; op : t -> t }.
 
 Canonical Structure OpType : Op := Build_Op Type (fun X => X).
@@ -7,5 +5,5 @@ Canonical Structure OpType : Op := Build_Op Type (fun X => X).
 Lemma test1 (X:Type) : eq (op OpType X)  X.
 Proof eq_refl.
 
-Lemma test2 (A:Type) : eq (op _ A)  A.
-Fail Proof eq_refl.
+Definition test2 (A:Type) : eq (op _ A)  A.
+Proof eq_refl.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/4205.v b/test-suite/bugs/closed/4205.v
new file mode 100644
index 0000000000..c40dfcc1f3
--- /dev/null
+++ b/test-suite/bugs/closed/4205.v
@@ -0,0 +1,8 @@
+(* Testing a regression from 8.5beta1 to 8.5beta2 in evar-evar tactic unification problems *)
+
+
+Inductive test : nat -> nat -> nat -> nat -> Prop :=
+  | test1 : forall m n, test m n m n.
+
+Goal test 1 2 3 4.
+erewrite f_equal2 with (f := fun k l => test _ _ k l).
diff --git a/test-suite/bugs/closed/4240.v b/test-suite/bugs/closed/4240.v
new file mode 100644
index 0000000000..083c59fe68
--- /dev/null
+++ b/test-suite/bugs/closed/4240.v
@@ -0,0 +1,12 @@
+(* Check that closure of filter did not restrict the former evar filter *)
+
+Lemma foo (new : nat) : False.
+evar (H1: nat).
+set (H3 := 0).
+assert (H3' := id H3).
+evar (H5: nat).
+clear H3.
+assert (H5 = new).
+unfold H5.
+unfold H1.
+exact (eq_refl new).
diff --git a/test-suite/bugs/closed/4276.v b/test-suite/bugs/closed/4276.v
new file mode 100644
index 0000000000..ba82e6c376
--- /dev/null
+++ b/test-suite/bugs/closed/4276.v
@@ -0,0 +1,11 @@
+Set Primitive Projections.
+
+Record box (T U : Type) (x := T) := wrap { unwrap : T }.
+Definition mybox : box True False := wrap _ _ I.
+Definition unwrap' := @unwrap.
+
+Definition bad' : True := mybox.(unwrap _ _). 
+
+Fail Definition bad : False := unwrap _ _ mybox.
+
+(* Closed under the global context *)
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/4283.v b/test-suite/bugs/closed/4283.v
new file mode 100644
index 0000000000..e06998b711
--- /dev/null
+++ b/test-suite/bugs/closed/4283.v
@@ -0,0 +1,8 @@
+Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unwrap) := b in unwrap.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl.
+