From 6e22ae3f21ae32f298b6e3463448f59a5c7d1f76 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 29 Sep 2014 00:10:43 +0200
Subject: 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.

---
 test-suite/bugs/closed/3566.v |  3 ++-
 test-suite/bugs/closed/3625.v |  9 ++++++++
 test-suite/bugs/closed/3660.v | 27 +++++++++++++++++++++++
 test-suite/bugs/closed/3666.v | 50 +++++++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/3667.v |  4 ++--
 test-suite/bugs/opened/3461.v |  3 ++-
 test-suite/bugs/opened/3625.v |  7 ------
 test-suite/bugs/opened/3660.v | 27 -----------------------
 8 files changed, 92 insertions(+), 38 deletions(-)
 create mode 100644 test-suite/bugs/closed/3625.v
 create mode 100644 test-suite/bugs/closed/3660.v
 create mode 100644 test-suite/bugs/closed/3666.v
 delete mode 100644 test-suite/bugs/opened/3625.v
 delete mode 100644 test-suite/bugs/opened/3660.v

(limited to 'test-suite')

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/closed/3625.v b/test-suite/bugs/closed/3625.v
new file mode 100644
index 0000000000..a0f977eeae
--- /dev/null
+++ b/test-suite/bugs/closed/3625.v
@@ -0,0 +1,9 @@
+Set Implicit Arguments.
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+
+Goal forall x y : prod Set Set, x.(@fst _ _) = y.(@fst _ _).
+ intros.
+ apply f_equal.
+ admit.
+Qed.
diff --git a/test-suite/bugs/closed/3660.v b/test-suite/bugs/closed/3660.v
new file mode 100644
index 0000000000..ed8964ce11
--- /dev/null
+++ b/test-suite/bugs/closed/3660.v
@@ -0,0 +1,27 @@
+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.
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).
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.
-- 
cgit v1.2.3