blob: 6de3ebdbd4bf159fbc15020cee5af6a707d7ef03 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Set Primitive Projections.
Set Implicit Arguments.
Set Universe Polymorphism.
Record category :=
{ ob :> Type;
hom : ob -> ob -> Type
}.
Record foo := { C : category; x :> ob C }.
(* Toplevel input, characters 0-42:
Error: Cannot find the target class. *)
|
