diff options
Diffstat (limited to 'doc/sphinx/using/libraries')
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 917edf0774..7461bfe443 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -22,13 +22,17 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` by a comma. This attribute is supported by the following commands: :cmd:`Ltac`, - :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`, :cmd:`Ltac2`, + :cmd:`Ltac2 Notation`, :cmd:`Ltac2 external`. 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. + Ltac2 definition @qualid is deprecated since @string__since. @string__note. + Ltac2 alias @qualid is deprecated since @string__since. @string__note. + Ltac2 notation {+ @ltac2_scope } 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 |