diff options
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_082.v (renamed from test-suite/bugs/opened/HoTT_coq_082.v) | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_082.v b/test-suite/bugs/closed/HoTT_coq_082.v index 257afe0b6e..ccba22cae5 100644 --- a/test-suite/bugs/opened/HoTT_coq_082.v +++ b/test-suite/bugs/closed/HoTT_coq_082.v @@ -4,7 +4,7 @@ Set Universe Polymorphism. Record category := { ob : Type }. -Fail Existing Class category. (* +Existing Class category. (* Toplevel input, characters 0-24: Anomaly: Mismatched instance and context when building universe substitution. Please report. *) @@ -13,7 +13,7 @@ Record category' := { ob' : Type; hom' : ob' -> ob' -> Type }. -Fail Existing Class category'. (* +Existing Class category'. (* Toplevel input, characters 0-24: Anomaly: Mismatched instance and context when building universe substitution. Please report. *) |