blob: bcd12aa691709010dfd4d17369f2644cdce32359 (
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
}.
Fail Record foo := { C : category; x :> ob C }.
(* Toplevel input, characters 0-42:
Error: Cannot find the target class. *)
|
