Existing Class now works with universe polymorphism. Fixes HoTT bug #063

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.