diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-18 17:47:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-19 12:44:52 +0200 |
| commit | 83c17d79c3388ebd488559dcf99d5d019e60bb1c (patch) | |
| tree | 05019158cce1d1e362b54862ab27de356686b7b2 | |
| parent | 9f9b2c9ae114a6d707af7b9e04098f4fc83fd97e (diff) | |
HoTT coq bug #62 fixed.
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_062.v (renamed from test-suite/bugs/opened/HoTT_coq_062.v) | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v index 7f1908f08..db8953168 100644 --- a/test-suite/bugs/opened/HoTT_coq_062.v +++ b/test-suite/bugs/closed/HoTT_coq_062.v @@ -61,18 +61,18 @@ Section Univalence. := path_universe_uncurried (BuildEquiv _ _ f feq). End Univalence. -Definition e : Bool <~> Bool. +Definition e : Equiv@{i j} Bool Bool. admit. Defined. -Definition p `{Univalence} : @paths Set Bool Bool := path_universe e. +Definition p `{Univalence} : @paths Type Bool Bool := path_universe e. -Theorem thm `{Univalence} : (forall A : Set, ((A -> False) -> False) -> A) -> False. +Theorem thm `{Univalence} : (forall A, ((A -> False) -> False) -> A) -> False. intro f. Set Printing Universes. Set Printing All. - pose proof (apD f p). - pose(path_universe e). + Show Universes. + pose proof (apD f p). pose proof (apD f (path_universe e)). admit. Defined. (* ??? Toplevel input, characters 0-37: |