From 7de7fe612ffc5a598311f9542e57e50803ff2007 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Oct 2020 15:32:54 +0200
Subject: [doc] attribute #[using]

---
 doc/sphinx/proof-engine/proof-handling.rst | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

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

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index b09d6146d8..f4aef8f879 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -199,6 +199,32 @@ list of assertion commands is given in :ref:`Assertions`. The command
 
    .. seealso:: :ref:`tactics-implicit-automation`
 
+.. attr:: using
+
+   This attribute can be applied to the :cmd:`Definition`, :cmd:`Example`,
+   :cmd:`Fixpoint` and :cmd:`CoFixpoint` commands as well as to :cmd:`Lemma` and
+   its variants.  It takes
+   a :n:`@section_var_expr`, in quotes, as its value. This is equivalent to
+   specifying the same :n:`@section_var_expr` in
+   :cmd:`Proof using`.
+
+   .. example::
+
+      .. coqtop:: all
+
+         Section Test.
+         Variable n : nat.
+         Hypothesis Hn : n <> 0.
+
+         #[using="Hn"]
+         Lemma example : 0 < n.
+
+      .. coqtop:: in
+
+         Abort.
+         End Test.
+
+
 Proof using options
 ```````````````````
 
-- 
cgit v1.2.3