diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_063.v (renamed from test-suite/bugs/opened/HoTT_coq_063.v) | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_063.v b/test-suite/bugs/closed/HoTT_coq_063.v index 8656fadaa9..777f6483d5 100644 --- a/test-suite/bugs/opened/HoTT_coq_063.v +++ b/test-suite/bugs/closed/HoTT_coq_063.v @@ -8,9 +8,13 @@ Module A. | 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. *) + Existing Class IsTrunc. + + + Instance is_trunc_unit : IsTrunc 0 unit. + Proof. apply BuildContr with (center:=tt). now intros []. Defined. + + Check (_ : IsTrunc 0 unit). End A. Module B. @@ -20,7 +24,11 @@ Module B. | S _ => False end. - Fail Existing Class IsTrunc. - (* Anomaly: Mismatched instance and context when building universe substitution. -Please report. *) + Existing Class IsTrunc. + + Instance is_trunc_unit : IsTrunc 0 unit. + Proof. exact I. Defined. + + Check (_ : IsTrunc 0 unit). + Fail Definition foo := (_ : IsTrunc 1 unit). End B. |