blob: ccba22cae547f2a1ff2e60f59df39a97f257958b (
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 }.
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 }.
Existing Class category'. (*
Toplevel input, characters 0-24:
Anomaly: Mismatched instance and context when building universe substitution.
Please report. *)
|
