diff options
| author | Matthieu Sozeau | 2014-06-17 16:14:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-17 17:19:03 +0200 |
| commit | 8fa5a0351954cc561fa751901fe0f06eeac4ce7a (patch) | |
| tree | 2d09d6543fea93fb9e3da09fa67f9d2978074928 | |
| parent | 527a09cc27ac64ab308220b25eb683a882dbddc1 (diff) | |
HoTT coq bug #82 already fixed.
| -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. *) |