blob: 96814a1b975271b1596462339da9665b65a23d5e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
Module Syndefs.
#[deprecated(since = "8.9", note = "Do not use.")]
Notation foo := Prop.
Notation bar := Prop (compat "8.9").
Fail
#[deprecated(since = "8.9", note = "Do not use.")]
Notation zar := Prop (compat "8.9").
Check foo.
Check bar.
Set Warnings "+deprecated".
Fail Check foo.
Fail Check bar.
End Syndefs.
Module Notations.
#[deprecated(since = "8.9", note = "Do not use.")]
Notation "!!" := Prop.
Notation "##" := Prop (compat "8.9").
Fail
#[deprecated(since = "8.9", note = "Do not use.")]
Notation "**" := Prop (compat "8.9").
Check !!.
Check ##.
Set Warnings "+deprecated".
Fail Check !!.
Fail Check ##.
End Notations.
Module Infix.
#[deprecated(since = "8.9", note = "Do not use.")]
Infix "!!" := plus (at level 1).
Infix "##" := plus (at level 1, compat "8.9").
Fail
#[deprecated(since = "8.9", note = "Do not use.")]
Infix "**" := plus (at level 1, compat "8.9").
Check (_ !! _).
Check (_ ## _).
Set Warnings "+deprecated".
Fail Check (_ !! _).
Fail Check (_ ## _).
End Infix.
|
