diff options
| author | Matthieu Sozeau | 2014-06-17 17:03:25 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-17 17:19:04 +0200 |
| commit | 40c2154e369cf1a3434fe34679bb3a186df3199a (patch) | |
| tree | 81118ebda2f219e840dcf24bb6d3b32fb2d24e34 | |
| parent | bd755284f3fcdf7f2fced477b81d64d72226a38f (diff) | |
Not considering test-suite file #89 as a bug anymore.
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_089.v (renamed from test-suite/bugs/opened/HoTT_coq_089.v) | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_089.v b/test-suite/bugs/closed/HoTT_coq_089.v index 143f60404e..6841d6b279 100644 --- a/test-suite/bugs/opened/HoTT_coq_089.v +++ b/test-suite/bugs/closed/HoTT_coq_089.v @@ -3,7 +3,7 @@ Set Printing Universes. Inductive type_paths (A : Type) : Type -> Prop := idtypepath : type_paths A A. -Monomorphic Definition comp_type_paths := Eval compute in type_paths. +Monomorphic Definition comp_type_paths := Eval compute in type_paths@{Type Type}. Check comp_type_paths. (* comp_type_paths : Type (* Top.12 *) -> Type (* Top.12 *) -> Prop *) @@ -29,7 +29,7 @@ Defined. Goal Type. Proof. - Fail match type of comp_type_paths with + match type of comp_type_paths with | ?U0 -> ?U1 -> ?R => exact (@comp_type_paths nat U0) end. @@ -39,5 +39,5 @@ The term "Type (* Top.51 *)" has type "Type (* Top.51+1 *)" while it is expected to have type "Type (* Top.51 *)" (Universe inconsistency: Cannot enforce Top.51 < Top.51 because Top.51 = Top.51)). *) - admit. + Defined. |