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.

3 files changed, 2 insertions, 35 deletions

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).
diff --git a/test-suite/bugs/opened/3625.v b/test-suite/bugs/opened/3625.v
deleted file mode 100644
index 46a6c009eb..0000000000
--- a/test-suite/bugs/opened/3625.v
+++ /dev/null
@@ -1,7 +0,0 @@
-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. *)
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v
deleted file mode 100644
index ed8964ce11..0000000000
--- a/test-suite/bugs/opened/3660.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Generalizable All Variables.
-Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
-Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
-Open Scope function_scope.
-Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
-Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
-Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
-Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
-Axiom IsHSet : Type -> Type.
-Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000.
-admit.
-Defined.
-Set Primitive Projections.
-Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
-Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
-Global Instance isequiv_ap_setT X Y : IsEquiv (@ap _ _ setT X Y).
-admit.
-Defined.
-Local Open Scope equiv_scope.
-Axiom equiv_path : forall (A B : Type) (p : A = B), A <~> B.
-
-Goal forall (C D : hSet), IsEquiv (fun x : C = D => (equiv_path C D (ap setT x))).
-  intros.
-  change (IsEquiv (equiv_path C D o @ap _ _ setT C D)).
-  apply @isequiv_compose; [ | admit ].
-  Set Typeclasses Debug. 
-  typeclasses eauto.