blob: 257afe0b6eb51ea5d2fc7e33a2003fa7ad3345dc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Set Implicit Arguments.
Set Universe Polymorphism.
Record category :=
{ ob : Type }.
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 }.
Fail Existing Class category'. (*
Toplevel input, characters 0-24:
Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)
|
