From 024a7ab20b06d82571c68c3d2ac32cb60fb0053a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 16:02:35 +0200
Subject: test-suite: Fix test-suite Makefile

Using relative path for coqlib, for some reason this fails on Mac OS
X. Took the easiest way to fix it.
---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 476d850ac9..d2466250ab 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
-- 
cgit v1.2.3


From 7c7726a798caa6b506a727703de24d2bb5bb3956 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:04:45 +0200
Subject: Univs: bug fix.

Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
---
 test-suite/success/polymorphism.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index dc22b03f2d..957612ef1d 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
-- 
cgit v1.2.3


From 3264fdaa71b2327a992286a08df0dfbcf78ea4fe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:31:04 +0200
Subject: Checker: Fix bug #4282

Adapt to new [projection] abstract type comprising a constant and
a boolean.
---
 test-suite/coqchk/primproj.v | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 test-suite/coqchk/primproj.v

(limited to 'test-suite')

diff --git a/test-suite/coqchk/primproj.v b/test-suite/coqchk/primproj.v
new file mode 100644
index 0000000000..04d0a2b6f7
--- /dev/null
+++ b/test-suite/coqchk/primproj.v
@@ -0,0 +1,2 @@
+Set Primitive Projections.
+Record foo (T : Type) := { bar : T}.
-- 
cgit v1.2.3


From e1f5a499c43ec0d7b7ebe696941217fb503e2596 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jul 2015 16:09:29 +0200
Subject: Kernel: primitive projections handling of let-ins

Fixes bug #4176 (actually two bugs in one)

Correct computation of the type of primitive projections in presence of
let-ins.
---
 test-suite/bugs/closed/4276.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/bugs/closed/4276.v

(limited to 'test-suite')

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
-- 
cgit v1.2.3


From 2c59d19ad207a6bf193e9f0c9d73258b3133d484 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jul 2015 16:58:06 +0200
Subject: Kernel/Checker: Cleanup fixes of substitutions due to let-ins.

Avoid undeeded large substitutions, and add test-suite file for
fixed bug 4283 in closed/
---
 test-suite/bugs/closed/4283.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/4283.v

(limited to 'test-suite')

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.
+
-- 
cgit v1.2.3


From 6a15394c542e5f16bce9b75fc033397c454f47e9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 16 Jul 2015 19:24:23 +0200
Subject: Test file for #3819.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3819.v b/test-suite/bugs/closed/3819.v
new file mode 100644
index 0000000000..355d23a58b
--- /dev/null
+++ b/test-suite/bugs/closed/3819.v
@@ -0,0 +1,9 @@
+Record Op := { t : Type ; op : t -> t }.
+
+Canonical Structure OpType : Op := Build_Op Type (fun X => X).
+
+Lemma test1 (X:Type) : eq (op OpType X)  X.
+Proof eq_refl.
+
+Definition test2 (A:Type) : eq (op _ A)  A.
+Proof eq_refl.
\ No newline at end of file
-- 
cgit v1.2.3


From 8591217a89f0b71e8175752dc55c42a5b89fccec Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 20:21:58 +0200
Subject: Fixing bug #4240 (closure_of_filter was not ensuring refinement of
 former filter after 48509b61 and 3cd718c, because filtered let-ins were not
 any longer preserved).

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

(limited to 'test-suite')

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).
-- 
cgit v1.2.3


From 916a8dc2c6b1dd8400d5c44b5d9c7fc793cc0e97 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 16 Jul 2015 21:40:42 +0200
Subject: Remove old test file for #3819 (now fixed).

---
 test-suite/bugs/opened/3819.v | 11 -----------
 1 file changed, 11 deletions(-)
 delete mode 100644 test-suite/bugs/opened/3819.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/opened/3819.v
deleted file mode 100644
index 7105a65877..0000000000
--- a/test-suite/bugs/opened/3819.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Set Universe Polymorphism.
-
-Record Op := { t : Type ; op : t -> t }.
-
-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.
-- 
cgit v1.2.3


From fdd6a17b272995237c9f95fc465bb1ff6871bedc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 22:53:10 +0200
Subject: Refining 71def2f8 on too strong occur-check limiting evar-evar
 unification in tactics.

The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.

Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.
---
 test-suite/bugs/closed/4205.v | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 test-suite/bugs/closed/4205.v

(limited to 'test-suite')

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).
-- 
cgit v1.2.3