diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 16:08:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:04 +0200 |
| commit | 84544396cbbf34848be2240acf181b4d5f1f42d2 (patch) | |
| tree | 72d398f334bdc7b1c6a0ee333a05940c34780f12 /test-suite | |
| parent | 0efba04058ba28889c83553224309be216873298 (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/opened/3660.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v index f962e1f04..ed8964ce1 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. |