From 701a69732ef2abfc7384296e090a3e9bd7604bbd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 Nov 2015 18:45:32 +0100
Subject: Fixing bug #3554: Anomaly: Anonymous implicit argument.

We just handle unnamed implicits using a dummy name. Note that the implicit
argument logic should still output warnings whenever the user writes implicit
arguments that won't be taken into account, but I'll leave that for another
time.
---
 test-suite/bugs/closed/3554.v | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 test-suite/bugs/closed/3554.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3554.v b/test-suite/bugs/closed/3554.v
new file mode 100644
index 0000000000..13a79cc840
--- /dev/null
+++ b/test-suite/bugs/closed/3554.v
@@ -0,0 +1 @@
+Example foo (f : forall {_ : Type}, Type) : Type.
-- 
cgit v1.2.3


From 2f56f0fcf21902bb1317f1d6f7ba4b593d712646 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 16:04:43 -0500
Subject: Fix bug #4293: ensure let-ins do not contain algebraic universes in
 their type annotation.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v
new file mode 100644
index 0000000000..3671c931b7
--- /dev/null
+++ b/test-suite/bugs/closed/4293.v
@@ -0,0 +1,7 @@
+Module Type Foo.
+Definition T := let X := Type in Type.
+End Foo.
+
+Module M : Foo.
+Definition T := let X := Type in Type.
+End M.
\ No newline at end of file
-- 
cgit v1.2.3


From ca30a8be08beeae77d42b6cb5d9f219e3932a3f7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:12:39 -0500
Subject: Fix bug #3257, setoid_reflexivity should fail if not completing the
 goal.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3257.v b/test-suite/bugs/closed/3257.v
new file mode 100644
index 0000000000..d8aa6a0479
--- /dev/null
+++ b/test-suite/bugs/closed/3257.v
@@ -0,0 +1,5 @@
+Require Import Setoid Morphisms Basics.
+Lemma foo A B (P : B -> Prop) :
+  pointwise_relation _ impl (fun z => A -> P z) P.
+Proof.
+  Fail reflexivity.
-- 
cgit v1.2.3


From 7de9c1a45a354676a073e216f42c34820e454691 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 11 Nov 2015 20:39:41 +0100
Subject: Now closed.

---
 test-suite/bugs/opened/3554.v | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 test-suite/bugs/opened/3554.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/3554.v b/test-suite/bugs/opened/3554.v
deleted file mode 100644
index 422c5770ea..0000000000
--- a/test-suite/bugs/opened/3554.v
+++ /dev/null
@@ -1 +0,0 @@
-Fail Example foo (f : forall {_ : Type}, Type) : Type.
-- 
cgit v1.2.3


From db002583b18c8742c0cd8e1a12305166b6b791ce Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 12 Nov 2015 12:05:00 +0100
Subject: Fixed test-suite file for bug #3998.

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v
new file mode 100644
index 0000000000..ced13839dd
--- /dev/null
+++ b/test-suite/bugs/closed/3998.v
@@ -0,0 +1,24 @@
+Class FieldType (F : Set) := mkFieldType { fldTy: F -> Set }.
+Hint Mode FieldType + : typeclass_instances. (* The F parameter is an input *)
+
+Inductive I1 := C.
+Inductive I2 := .
+
+Instance I1FieldType : FieldType I1 := { fldTy := I1_rect _ bool }.
+Instance I2FieldType : FieldType I2 := { fldTy := I2_rect _ }.
+
+Definition RecordOf F (FT: FieldType F) := forall f:F, fldTy f.
+
+Class MapOps (M K : Set) := {
+  tgtTy: K -> Set;
+  update: M -> forall k:K, tgtTy k -> M
+}.
+
+Instance RecordMapOps F (FT: FieldType F) : MapOps (RecordOf F FT) F :=
+{ tgtTy := fldTy; update := fun r (f: F) (x: fldTy f) z => r z }.
+
+Axiom ex : RecordOf _ I1FieldType.
+
+Definition works := (fun ex' => update ex' C true) (update ex C false).
+Set Typeclasses Debug.
+Definition doesnt := update (update ex C false) C true.
\ No newline at end of file
-- 
cgit v1.2.3


From 0c11bc39927c7756a0e3c3a6c445f20d0daaad7f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 12 Nov 2015 14:14:38 +0100
Subject: Fix bug #4412: [rewrite] (setoid_rewrite?) creates ill-typed terms.

We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
---
 test-suite/bugs/closed/4412.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/closed/4412.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4412.v b/test-suite/bugs/closed/4412.v
new file mode 100644
index 0000000000..4b2aae0c7b
--- /dev/null
+++ b/test-suite/bugs/closed/4412.v
@@ -0,0 +1,4 @@
+Require Import Coq.Bool.Bool Coq.Setoids.Setoid.
+Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True.
+  intros.
+  Fail rewrite Bool.andb_true_iff in H.
-- 
cgit v1.2.3