blob: c074f1cfc1b59dd96fd7e1d28d2cd249e1bf54b0 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Record foo := { f : Type }.
Fail Canonical Structure xx@{} := {| f := Type |}.
Canonical Structure xx@{i} := {| f := Type@{i} |}.
Fail Coercion cc@{} := fun x : Type => Build_foo x.
Coercion cc@{i} := fun x : Type@{i} => Build_foo x.
|
