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