From 84544396cbbf34848be2240acf181b4d5f1f42d2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 27 Sep 2014 16:08:02 +0200
Subject: Add a boolean to indicate the unfolding state of a primitive
 projection, so as to reproduce correctly the reduction behavior of existing
 projections, i.e. delta + iota. Make [projection] an abstract datatype in
 Names.ml, most of the patch is about using that abstraction. Fix
 unification.ml which tried canonical projections too early in presence of
 primitive projections.

---
 test-suite/bugs/opened/3660.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v
index f962e1f048..ed8964ce11 100644
--- a/test-suite/bugs/opened/3660.v
+++ b/test-suite/bugs/opened/3660.v
@@ -18,10 +18,10 @@ 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 ].
-  solve [ apply isequiv_ap_setT ].
-  Undo.
-  Fail typeclasses eauto.
+  Set Typeclasses Debug. 
+  typeclasses eauto.
-- 
cgit v1.2.3