From 234a802f0925f9c9078417afa28dcb00c31668d9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 21 Jan 2021 16:54:19 +0100
Subject: Add documentation.

---
 doc/sphinx/proof-engine/ltac2.rst | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 9f3f0ef3d5..83d8ebf757 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
-- 
cgit v1.2.3