blob: 60d40d3d1265d1c51ab56994709afc98631495ec (
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
|
Module Syndefs.
#[deprecated(since = "8.9", note = "Do not use.")]
Notation foo := Prop.
Check foo.
Set Warnings "+deprecated".
Fail Check foo.
End Syndefs.
Module Notations.
#[deprecated(since = "8.9", note = "Do not use.")]
Notation "!!" := Prop.
Check !!.
Set Warnings "+deprecated".
Fail Check !!.
End Notations.
Module Infix.
#[deprecated(since = "8.9", note = "Do not use.")]
Infix "!!" := plus (at level 1).
Check (_ !! _).
Set Warnings "+deprecated".
Fail Check (_ !! _).
End Infix.
|
