Merge PR #13183: attribute #[using] for Definition and Fixpoint

Reviewed-by: SkySkimmer
Ack-by: herbelin
Ack-by: Zimmi48

5 files changed, 40 insertions, 4 deletions

diff --git a/doc/changelog/02-specification-language/13183-using-att.rst b/doc/changelog/02-specification-language/13183-using-att.rst
new file mode 100644
index 0000000000..c380d932ed
--- /dev/null
+++ b/doc/changelog/02-specification-language/13183-using-att.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Definition and (Co)Fixpoint now support the :attr:`using` attribute.
+  It has the same effect as :cmd:`Proof using`, which is only available in
+  interactive mode.
+  (`#13183 <https://github.com/coq/coq/pull/13183>`_,
+  by Enrico Tassi).
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index 0520afd600..2e5dff42ac 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -28,8 +28,8 @@ More information on co-inductive definitions can be found in
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(monomorphic)`, :attr:`universes(template)`,
    :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)` and :attr:`private(matching)`
-   attributes.
+   :attr:`universes(noncumulative)`, :attr:`private(matching)`
+   and :attr:`using` attributes.
 
 .. example::
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 8d67a3cf40..1681eee6e7 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -87,8 +87,8 @@ Section :ref:`typing-rules`.
    computation on :n:`@term`.
 
    These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`) and
-   :attr:`canonical` attributes.
+   :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`),
+   :attr:`canonical` and :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
@@ -159,6 +159,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
+   This command accepts the :attr:`using` attribute.
+
    .. exn:: The term @term has type @type which should be Set, Prop or Type.
       :undocumented:
 
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index ba0ec28f8b..1642482bb1 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -416,6 +416,8 @@ constructions.
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
 
+   This command accepts the :attr:`using` attribute.
+
    .. note::
 
       + Some fixpoints may have several arguments that fit as decreasing
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
 ```````````````````