blob: c85f8129cea98b0f07f87f0508bcb29ad989d206 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
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.
Polymorphic Coercion cc@{i} := fun x : Type@{i} => Build_foo x.
Coercion cc1@{i} := (cc@{i}).
|
