Merge branch 'v8.5'

8 files changed, 56 insertions, 5 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 476d850ac..d2466250a 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -28,7 +28,7 @@
 # Default value when called from a freshly compiled Coq, but can be
 # easily overridden
 BIN := ../bin/
-LIB := ..
+LIB := $(shell cd ..; pwd)
 
 coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
 bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/closed/3819.v
index 7105a6587..355d23a58 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 000000000..c40dfcc1f
--- /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 000000000..083c59fe6
--- /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 000000000..ba82e6c37
--- /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 000000000..e06998b71
--- /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.
+
diff --git a/test-suite/coqchk/primproj.v b/test-suite/coqchk/primproj.v
new file mode 100644
index 000000000..04d0a2b6f
--- /dev/null
+++ b/test-suite/coqchk/primproj.v
@@ -0,0 +1,2 @@
+Set Primitive Projections.
+Record foo (T : Type) := { bar : T}.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index dc22b03f2..957612ef1 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -308,3 +308,15 @@ Definition RLRL' : forall x : R, RL x = RL (RL x).
 Qed.
 
 End eta.
+
+Module Hurkens'.
+  Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
+Type)) eq_refl.
+
+End Hurkens'.
\ No newline at end of file