3 files changed, 66 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2590.v b/test-suite/bugs/closed/2590.v
new file mode 100644
index 000000000..e594e9693
--- /dev/null
+++ b/test-suite/bugs/closed/2590.v
@@ -0,0 +1,19 @@
+Require Import Relation_Definitions RelationClasses Setoid SetoidClass.
+
+Section Bug.
+
+  Context {A : Type} (R : relation A).
+  Hypothesis pre : PreOrder R.
+  Context `{SA : Setoid A}.
+
+  Goal True.
+  set (SA' := SA).
+    assert ( forall SA0 : Setoid A,
+               @PartialOrder A (@equiv A SA0) (@setoid_equiv A SA0) R pre ).
+    rename SA into SA0.
+    intro SA.
+    admit.
+    admit.
+Qed.
+End Bug.
+
diff --git a/test-suite/bugs/closed/3560.v b/test-suite/bugs/closed/3560.v
new file mode 100644
index 000000000..65ce4fb6b
--- /dev/null
+++ b/test-suite/bugs/closed/3560.v
@@ -0,0 +1,15 @@
+
+(* File reduced by coq-bug-finder from original input, then from 6236 lines to 1049 lines, then from 920 lines to 209 lines, then from 179 lines to 30 lines *)
+(* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml 4.01.0
+   coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *)
+
+Set Primitive Projections.
+Set Implicit Arguments.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Notation "x * y" := (prod x y) : type_scope.
+Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv : forall P, P equiv_fun }.
+Goal forall (A B : Type) (C : Type), Equiv (A -> B -> C) (A * B -> C).
+Proof.
+  intros.
+  exists (fun u => fun x => u (fst x) (snd x)).
+Abort.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v
new file mode 100644
index 000000000..33ca9651a
--- /dev/null
+++ b/test-suite/bugs/closed/3783.v
@@ -0,0 +1,32 @@
+Fixpoint exp (n : nat) (T : Set)
+  := match n with
+       | 0 => T
+       | S n' => exp n' (T * T)
+     end.
+Definition big := Eval compute in exp 13 nat.
+Module NonPrim.
+  Unset Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Time cbv beta in y. (* 0s *)
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Timeout 1 cbv beta in y. (* takes around 2s.  Grows with the value passed to [exp] above *)
+    admit.
+  Defined.
+End Prim.
+\ No newline at end of file