Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations

Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle

2 files changed, 13 insertions, 2 deletions

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 146da8bb37..294c56ef06 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -66,7 +66,6 @@ Current limitations include:
   - An easy way to get the number of constructors of an inductive type.
     Currently only way to do this is to destruct a variable of the inductive type
     and count the number of goals that result.
-- The :attr:`deprecated` attribute is not supported for Ltac2 definitions.
 
 - Error messages may be cryptic.
 
@@ -229,6 +228,8 @@ One can define new types with the following commands.
    defined in Coq and give their type information.  They can also declare
    data structures from OCaml.  This command has no use for the end user.
 
+   This command supports the :attr:`deprecated` attribute.
+
 APIs
 ~~~~
 
@@ -319,6 +320,8 @@ Ltac2 Definitions
 
    If ``mutable`` is set, the definition can be redefined at a later stage (see below).
 
+   This command supports the :attr:`deprecated` attribute.
+
 .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr
 
    This command redefines a previous ``mutable`` definition.
@@ -1246,6 +1249,8 @@ Notations
       so that you may have to resort to thunking to ensure that side-effects are
       performed at the right time.
 
+   This command supports the :attr:`deprecated` attribute.
+
 Abbreviations
 ~~~~~~~~~~~~~
 
@@ -1276,6 +1281,8 @@ Abbreviations
    Note that abbreviations are not type checked at all, and may result in typing
    errors after expansion.
 
+   This command supports the :attr:`deprecated` attribute.
+
 .. _defining_tactics:
 
 Defining tactics
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