In evarconv and unification, expand folded primitive projections to

their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.

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).