diff options
| author | Michael Soegtrop | 2021-03-23 21:55:59 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2021-03-23 21:55:59 +0100 |
| commit | 47c20236f578dca9381822a62b5a406d6b42676d (patch) | |
| tree | fef686014dc1985799869ff1d6cab4e8f76ec8bc /doc/sphinx/using/libraries | |
| parent | fa2ba1571cbd791c3b1acd87adeacd0aa4bd6e88 (diff) | |
| parent | 83c11db006ca87b3912d2548593b669884a3b4b5 (diff) | |
Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
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 |