10 files changed, 47 insertions, 12 deletions

diff --git a/doc/changelog/02-specification-language/13183-using-att.rst b/doc/changelog/02-specification-language/13183-using-att.rst
index 9b09bf2383..c380d932ed 100644
--- a/doc/changelog/02-specification-language/13183-using-att.rst
+++ b/doc/changelog/02-specification-language/13183-using-att.rst
@@ -1,5 +1,5 @@
 - **Added:**
-  Attribute :attr:`using` now supported by Definition and (Co)Fixpoint.
+  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>`_,
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
 ```````````````````
 
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index c55a7928d9..efba6d332a 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -229,6 +229,6 @@ let uses_parser : string key_parser = fun orig args ->
   assert_once ~name:"using" orig;
   match args with
   | VernacFlagLeaf str -> str
-  |  _ -> CErrors.user_err (Pp.str "Ill formed uses attribute")
+  |  _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
 
 let using = attribute_of_list ["using",uses_parser]
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index aa71e58cf6..3fc74cba5b 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -121,7 +121,8 @@ let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ct
   let using = using |> Option.map (fun expr ->
     let terms = body :: match types with Some x -> [x] | None -> [] in
     let l = Proof_using.process_expr (Global.env()) evd expr terms in
-    Names.Id.Set.(List.fold_right add l empty)) in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
   let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
@@ -140,7 +141,8 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red
   let using = using |> Option.map (fun expr ->
     let terms = body :: match types with Some x -> [x] | None -> [] in
     let l = Proof_using.process_expr (Global.env()) evd expr terms in
-    Names.Id.Set.(List.fold_right add l empty)) in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
     let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index bd11fa2b47..29bf5fbcc2 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -263,7 +263,8 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps =
           let env = Global.env() in
           let sigma = Evd.from_env env in
           let l = Proof_using.process_expr env sigma expr terms in
-          Names.Id.Set.(List.fold_right add l empty)) in
+          Names.Id.Set.(List.fold_right add l empty))
+        in
         let args = List.map Context.Rel.Declaration.get_name ctx in
         Declare.CInfo.make ~name ~typ ~args ~impargs ?using ()
       ) fixnames fixtypes fiximps
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index c2e07c4fd5..9623317ddf 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -262,7 +262,8 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notat
   let using = using |> Option.map (fun expr ->
     let terms = List.map EConstr.of_constr [evars_def; evars_typ] in
     let l = Proof_using.process_expr env sigma expr terms in
-    Names.Id.Set.(List.fold_right add l empty)) in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let uctx = Evd.evar_universe_context sigma in
   let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
   let info = Declare.Info.make ~udecl ~poly ~hook () in
@@ -294,7 +295,8 @@ let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
     let using = using |> Option.map (fun expr ->
       let terms = [def; typ] in
       let l = Proof_using.process_expr env evd expr terms in
-      Names.Id.Set.(List.fold_right add l empty)) in
+      Names.Id.Set.(List.fold_right add l empty))
+    in
     let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b6e7d22732..bc03994ca6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -501,7 +501,7 @@ let program_inference_hook env sigma ev =
 let vernac_set_used_variables ~pstate e : Declare.Proof.t =
   let env = Global.env () in
   let sigma, _ = Declare.Proof.get_current_context pstate in
-  let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in
+  let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in
   let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in
   let l = Proof_using.process_expr env sigma e tys in
   let vars = Environ.named_context env in