blob: 91634ea023ce289c3613ed82a4078413a9b2ba99 (
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
|
.. attr:: deprecated ( {? since = @string , } {? note = @string } )
:name: deprecated
At least one of :n:`since` or :n:`note` must be present. If both are present,
either one may appear first and they must be separated by a comma.
This attribute is supported by the following commands: :cmd:`Ltac`,
:cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`.
It can trigger the following warnings:
.. warn:: Tactic @qualid is deprecated since @string__since. @string__note.
Tactic Notation @qualid is deprecated since @string__since. @string__note.
Notation @string is deprecated since @string__since. @string__note.
:n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number,
:n:`@string__note` is the note (usually explains the replacement).
.. example::
.. coqtop:: all reset warn
#[deprecated(since="8.9.0", note="Use idtac instead.")]
Ltac foo := idtac.
Goal True.
Proof.
now foo.
Abort.
|
