diff options
| author | Matthieu Sozeau | 2014-06-13 14:38:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-13 17:40:27 +0200 |
| commit | f49137b917fa7561eb53a87155ed57b3dbc70d90 (patch) | |
| tree | 4d209f1fa70c0204074c691e3b2be579a7d8e999 | |
| parent | 1681238424c2d46e7a31467212d4daed4b30a827 (diff) | |
HoTT/coq bug #7 is closed, and the definitions can be made to go through using explicit
universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_007.v (renamed from test-suite/bugs/opened/HoTT_coq_007.v) | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v index f609aff5d7..8592c729d0 100644 --- a/test-suite/bugs/opened/HoTT_coq_007.v +++ b/test-suite/bugs/closed/HoTT_coq_007.v @@ -25,7 +25,7 @@ Module Comment1. intros; autorewrite with functor; reflexivity. Defined. - Definition Cat0 : Category Empty_set. + Definition Cat0 : Category@{i j} Empty_set. refine {| Morphism := fun s d : Empty_set => s = d; Identity := fun o : Empty_set => eq_refl @@ -36,14 +36,11 @@ Module Comment1. Set Printing All. Set Printing Universes. - Fail Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). (** ??? The term "y" has type - "@Functor (* Top.448 Top.449 Top.450 Top.451 *) - (@Functor (* Set Top.441 Top.442 Top.336 *) Empty_set Cat0 objC C) C0 - Empty_set Cat0" while it is expected to have type - "@Functor (* Top.295 Top.296 Top.295 Top.296 *) ?46 ?47 ?48 ?49" -(Universe inconsistency: Cannot enforce Set = Top.295)). *) - Fail intro. (* Illegal application (Type Error) *) - Fail Abort. + Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) + : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). + intro. intro. + unfold ComposeFunctors. + Abort. End Comment1. Module Comment2. |