blob: 265310b1a340e3faac1c3ecd1b2ebc12f23fd615 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Structure type : Type := Pack { ob : Type }.
Polymorphic Record category := { foo : Type }.
Definition FuncComp := Pack category.
Axiom C : category.
Check (C : ob FuncComp). (* OK *)
Canonical Structure FuncComp.
Check (C : ob FuncComp).
(* Toplevel input, characters 15-39:
Error:
The term "C" has type "category" while it is expected to have type
"ob FuncComp". *)
|
