diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-17 11:18:10 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-17 15:42:14 +0200 |
| commit | b8834d66013b38cef247507f312bb081de04da27 (patch) | |
| tree | 13bf7e5c58c160eac0dafa6d36e9f7a9ad6745e9 /test-suite/bugs/opened | |
| parent | 0091c528cb1b0171215a6ef5a47f26763a4edc09 (diff) | |
Existing Class now works with universe polymorphism. Fixes HoTT bug #063
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_063.v | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_063.v b/test-suite/bugs/opened/HoTT_coq_063.v deleted file mode 100644 index 8656fadaa..000000000 --- a/test-suite/bugs/opened/HoTT_coq_063.v +++ /dev/null @@ -1,26 +0,0 @@ -Set Universe Polymorphism. -Module A. - Inductive paths A (x : A) : A -> Type := idpath : paths A x x. - - Notation "x = y" := (paths _ x y). - - Inductive IsTrunc : nat -> Type -> Type := - | BuildContr : forall A (center : A) (contr : forall y, center = y), IsTrunc 0 A - | trunc_S : forall A n, (forall x y : A, IsTrunc n (x = y)) -> IsTrunc (S n) A. - - Fail Existing Class IsTrunc. - (* Anomaly: Mismatched instance and context when building universe substitution. -Please report. *) -End A. - -Module B. - Fixpoint IsTrunc (n : nat) (A : Type) : Type := - match n with - | O => True - | S _ => False - end. - - Fail Existing Class IsTrunc. - (* Anomaly: Mismatched instance and context when building universe substitution. -Please report. *) -End B. |