blob: 5db3f9fadc38dd69fca82b762b5a2cbbe4a58c30 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Class A := {}.
Class B (x:A) := {}.
Class B' (a:=A) (x:a) := {}.
Fail Definition foo a `{B a} := 0.
Definition foo a `{B' a} := 0.
Record C (x:A) := {}.
Existing Class C.
Fail Definition bar a `{C a} := 0.
Definition X := Type.
Class Y (x:X) := {}.
Definition before `{Y Set} := 0.
Existing Class X.
Fail Definition after `{Y Set} := 0.
|
