From d483b7171dafadbe01520bbb6d0c75aa0d6099a7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 16 May 2014 19:25:16 +0200
Subject: Fix unification of non-unfoldable primitive projections in evarconv.

---
 pretyping/evarconv.ml                 | 12 ++++--------
 test-suite/bugs/closed/HoTT_coq_122.v | 25 +++++++++++++++++++++++++
 test-suite/bugs/opened/HoTT_coq_122.v | 25 -------------------------
 3 files changed, 29 insertions(+), 33 deletions(-)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_122.v
 delete mode 100644 test-suite/bugs/opened/HoTT_coq_122.v

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6bf621b055..aaf7ff65cc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -467,14 +467,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    ise_and i 
 	    [(fun i -> evar_conv_x ts env i CONV c c');
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
-	  and f2 i = 
-	    if is_transparent_constant ts p then
-	      match unfold_projection env p c sk1 with
-	      | Some (c, sk1) -> 
-		let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (c,sk1) in
-		  evar_eqappr_x ts env i pbty out1 (appr2, csts2)
-	      | None -> assert false
-	    else UnifFailure (i, NotSameHead)
+	  and f2 i =
+            let out1 = whd_betaiota_deltazeta_for_iota_state ts env i csts1 (v1,sk1)
+            and out2 = whd_betaiota_deltazeta_for_iota_state ts env i csts2 (v2,sk2)
+	    in evar_eqappr_x ts env i pbty out1 out2
 	  in
 	    ise_try evd [f1; f2]
 
diff --git a/test-suite/bugs/closed/HoTT_coq_122.v b/test-suite/bugs/closed/HoTT_coq_122.v
new file mode 100644
index 0000000000..1ba8e5c345
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_122.v
@@ -0,0 +1,25 @@
+(* File reduced by coq-bug-finder from original input, then from 669 lines to 79 lines, then from 89 lines to 44 lines *)
+Set Primitive Projections.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+
+Set Implicit Arguments.
+
+Record PreCategory :=
+  Build_PreCategory' {
+      object :> Type;
+      morphism : object -> object -> Type;
+
+      identity : forall x, morphism x x;
+      compose : forall s d d',
+                  morphism d d'
+                  -> morphism s d
+                  -> morphism s d'
+                              where "f 'o' g" := (compose f g);
+
+      left_identity : forall a b (f : morphism a b), identity b o f = f
+    }.
+
+Hint Rewrite @left_identity. (* stack overflow *)
diff --git a/test-suite/bugs/opened/HoTT_coq_122.v b/test-suite/bugs/opened/HoTT_coq_122.v
deleted file mode 100644
index 7e474d0a12..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_122.v
+++ /dev/null
@@ -1,25 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 669 lines to 79 lines, then from 89 lines to 44 lines *)
-Set Primitive Projections.
-Reserved Notation "g 'o' f" (at level 40, left associativity).
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-Notation "x = y" := (@paths _ x y) : type_scope.
-
-Set Implicit Arguments.
-
-Record PreCategory :=
-  Build_PreCategory' {
-      object :> Type;
-      morphism : object -> object -> Type;
-
-      identity : forall x, morphism x x;
-      compose : forall s d d',
-                  morphism d d'
-                  -> morphism s d
-                  -> morphism s d'
-                              where "f 'o' g" := (compose f g);
-
-      left_identity : forall a b (f : morphism a b), identity b o f = f
-    }.
-
-Fail Timeout 1 Hint Rewrite @left_identity. (* stack overflow *)
-- 
cgit v1.2.3