6 files changed, 61 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v
index e0075b8339..d71727be57 100644
--- a/test-suite/bugs/closed/3566.v
+++ b/test-suite/bugs/closed/3566.v
@@ -18,4 +18,5 @@ Definition lift {T} : T -> Lift T := fun x => x.
 
 Goal forall x y : Type, x = y.
   intros.
-  pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @ (@path_universe _ _ (@lift y) (H0 y))^)))%path as H''.
+  pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @ 
+                                                   (@path_universe _ _ (@lift y) (H0 y))^)))%path as H''.
diff --git a/test-suite/bugs/opened/3625.v b/test-suite/bugs/closed/3625.v
index 46a6c009eb..a0f977eeae 100644
--- a/test-suite/bugs/opened/3625.v
+++ b/test-suite/bugs/closed/3625.v
@@ -2,6 +2,8 @@ Set Implicit Arguments.
 Set Primitive Projections.
 Record prod A B := pair { fst : A ; snd : B }.
 
-Fail Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
-(*  intros.
-    apply f_equal. *)
+Goal forall x y : prod Set Set, x.(@fst _ _) = y.(@fst _ _).
+ intros.
+ apply f_equal.
+ admit.
+Qed.
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/closed/3660.v
index ed8964ce11..ed8964ce11 100644
--- a/test-suite/bugs/opened/3660.v
+++ b/test-suite/bugs/closed/3660.v
diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v
new file mode 100644
index 0000000000..a5b0e9347d
--- /dev/null
+++ b/test-suite/bugs/closed/3666.v
@@ -0,0 +1,50 @@
+(* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *)
+(* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
+
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V.
+Module NonPrim.
+  Record hProp := hp { hproptype :> Type ; isp : Set}.
+  Goal forall (A B : Type) (H_f : A -> V -> hProp) (H_g : B -> V -> hProp)
+              (C : Type) (h : C -> V) (b : B) (a : A) (c : C),
+         H_f a (h c) -> H_f a (h c) = H_g b (h c) -> H_g b (h c).
+    intros A B H_f H_g C h b a c H3 H'.
+    exact (@transport hProp (fun x => x) _ _ H' H3).
+    Undo.
+    Set Debug Unification.
+    exact (H' # H3).
+  Defined.
+End NonPrim.
+
+Module Prim.
+  Set Primitive Projections.
+  Set Universe Polymorphism.
+  Record hProp := hp { hproptype :> Type ; isp : Set}.
+  Goal forall (A B : Type) (H_f : A -> V -> hProp) (H_g : B -> V -> hProp)
+              (C : Type) (h : C -> V) (b : B) (a : A) (c : C),
+         H_f a (h c) -> H_f a (h c) = H_g b (h c) -> H_g b (h c).
+    intros A B H_f H_g C h b a c H3 H'.
+    exact (@transport hProp (fun x => x) _ _ H' H3).
+    Undo.
+    Set Debug Unification.
+    exact (H' # H3).
+    (* Toplevel input, characters 7-14:
+Error:
+In environment
+A : Type
+B : Type
+H_f : A -> V -> hProp
+H_g : B -> V -> hProp
+C : Type
+h : C -> V
+b : B
+a : A
+c : C
+H3 : H_f a (h c)
+H' : H_f a (h c) = H_g b (h c)
+Unable to unify "hproptype (H_f a (h c))" with "?T (H_f a (h c))".
+ *)
+  Defined.
+End Prim.
+\ No newline at end of file
diff --git a/test-suite/bugs/closed/3667.v b/test-suite/bugs/closed/3667.v
index e0d0e44863..d2fc4d9bf9 100644
--- a/test-suite/bugs/closed/3667.v
+++ b/test-suite/bugs/closed/3667.v
@@ -18,8 +18,8 @@ Definition set_cat : PreCategory.
                              (fun x y => x -> y))).
 Defined.
 Goal forall (A : PreCategory) (F : Functor A set_cat)
-            (a : A) (x : F a), x = x.
+            (a : A) (x : F a) (nt :NaturalTransformation F F), x = x.
   intros. 
-  pose (fun c d m => ap10 (commutes x c d m)).
+  pose (fun c d m => ap10 (commutes nt c d m)).
 
 
diff --git a/test-suite/bugs/opened/3461.v b/test-suite/bugs/opened/3461.v
index 1ca05a743f..1b625e6a15 100644
--- a/test-suite/bugs/opened/3461.v
+++ b/test-suite/bugs/opened/3461.v
@@ -1,4 +1,5 @@
 Lemma foo (b : bool) :
   exists x : nat, x = x.
 Proof.
-eexists; Fail eexact (eq_refl b).
+eexists. 
+Fail eexact (eq_refl b).