7 files changed, 72 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index ce21ff41c3..f41fb5b1e4 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -25,7 +25,7 @@
 # Includes
 ###########################################################################
 
-include ../config/Makefile
+-include ../config/Makefile
 include ../Makefile.common
 
 #######################################################################
diff --git a/test-suite/bugs/closed/4403.v b/test-suite/bugs/closed/4403.v
new file mode 100644
index 0000000000..a80f38fe2a
--- /dev/null
+++ b/test-suite/bugs/closed/4403.v
@@ -0,0 +1,3 @@
+(* -*- coq-prog-args: ("-type-in-type"); -*- *)
+
+Definition some_prop : Prop := Type.
diff --git a/test-suite/bugs/closed/5539.v b/test-suite/bugs/closed/5539.v
new file mode 100644
index 0000000000..48e5568e9b
--- /dev/null
+++ b/test-suite/bugs/closed/5539.v
@@ -0,0 +1,15 @@
+Set Universe Polymorphism.
+
+Inductive D : nat -> Type :=
+| DO : D O
+| DS n : D n -> D (S n).
+
+Fixpoint follow (n : nat) : D n -> Prop :=
+  match n with
+  | O => fun d => let 'DO := d in True
+  | S n' => fun d => (let 'DS _ d' := d in fun f => f d') (follow n')
+  end.
+
+Definition step (n : nat) (d : D n) (H : follow n d) :
+  follow (S n) (DS n d)
+  := H.
diff --git a/test-suite/bugs/closed/6951.v b/test-suite/bugs/closed/6951.v
new file mode 100644
index 0000000000..419f8d7c4e
--- /dev/null
+++ b/test-suite/bugs/closed/6951.v
@@ -0,0 +1,2 @@
+Record float2 : Set := Float2 { Fnum : unit }.
+Scheme Equality for float2.
diff --git a/test-suite/bugs/closed/7011.v b/test-suite/bugs/closed/7011.v
new file mode 100644
index 0000000000..296e4e11e5
--- /dev/null
+++ b/test-suite/bugs/closed/7011.v
@@ -0,0 +1,16 @@
+(* Fix and Cofix were missing in tactic unification *)
+
+Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end)
+               = (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end).
+Proof.
+  eexists.
+  reflexivity.
+Qed.
+
+CoInductive stream := cons : nat -> stream -> stream.
+
+Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo).
+Proof.
+  eexists.
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/7392.v b/test-suite/bugs/closed/7392.v
new file mode 100644
index 0000000000..cf465c6588
--- /dev/null
+++ b/test-suite/bugs/closed/7392.v
@@ -0,0 +1,9 @@
+Inductive R : nat -> Prop := ER : forall n, R n -> R (S n).
+
+Goal (forall (n : nat), R n -> False) -> True -> False.
+Proof.
+intros H0 H1.
+eapply H0.
+clear H1.
+apply ER.
+simpl.
diff --git a/test-suite/coqchk/bug_7539.v b/test-suite/coqchk/bug_7539.v
new file mode 100644
index 0000000000..74ebe9290d
--- /dev/null
+++ b/test-suite/coqchk/bug_7539.v
@@ -0,0 +1,26 @@
+Set Primitive Projections.
+
+CoInductive Stream : Type := Cons { tl : Stream }.
+
+Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream :=
+  match n with
+  | O => s
+  | S m => Str_nth_tl m (tl s)
+  end.
+
+CoInductive EqSt (s1 s2: Stream) : Prop := eqst {
+  eqst_tl : EqSt (tl s1) (tl s2);
+}.
+
+Axiom EqSt_reflex : forall (s : Stream), EqSt s s.
+
+CoFixpoint map (s:Stream) : Stream := Cons (map (tl s)).
+
+Lemma Str_nth_tl_map : forall n s, EqSt (Str_nth_tl n (map s)) (map (Str_nth_tl n s)).
+Proof.
+induction n.
++ intros; apply EqSt_reflex.
++ cbn; intros s; apply IHn.
+Qed.
+
+Definition boom : forall s, tl (map s) = map (tl s) := fun s => eq_refl.