Merge PR #7264: [Sphinx] Fix a lot of references and description of options

6 files changed, 196 insertions, 321 deletions

diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index ec1b942e0..19d4ba9ba 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -255,17 +255,16 @@ Displaying Available Coercions
 Activating the Printing of Coercions
 -------------------------------------
 
-.. cmd:: Set Printing Coercions.
+.. opt:: Printing Coercions
 
-  This command forces all the coercions to be printed.
-  Conversely, to skip the printing of coercions, use
-  ``Unset Printing Coercions``. By default, coercions are not printed.
+   When on, this option forces all the coercions to be printed.
+   By default, coercions are not printed.
 
-.. cmd:: Add Printing Coercion @qualid.
+.. cmd:: Add Printing Coercion @qualid
 
-  This command forces coercion denoted by `qualid` to be printed.
-  To skip the printing of coercion `qualid`, use
-  ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed.
+  This command forces coercion denoted by :n:`@qualid` to be printed. To skip
+  the printing of coercion :n:`@qualid`, use :cmd:`Remove Printing Coercion`. By
+  default, a coercion is never printed.
 
 .. _coercions-classes-as-records:
 
@@ -291,12 +290,9 @@ by extending the existing :cmd:`Record` macro. Its new syntax is:
    (this may fail if the uniform inheritance condition is not
    satisfied).
 
-.. note::
+.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
 
-  The keyword ``Structure`` is a synonym of ``Record``.
-
-..
-  FIXME: \comindex{Structure}
+   This is a synonym of :cmd:`Record`.
 
 
 Coercions and Sections
@@ -312,20 +308,17 @@ coercions which do not verify the uniform inheritance condition any longer
 are also forgotten.
 
 Coercions and Modules
---------------------=
-
-From |Coq| version 8.3, the coercions present in a module are activated
-only when the module is explicitly imported. Formerly, the coercions
-were activated as soon as the module was required, whatever it was
-imported or not.
-
-To recover the behavior of the versions of |Coq| prior to 8.3, use the
-following command:
+---------------------
 
-.. cmd:: Set Automatic Coercions Import.
+.. opt:: Automatic Coercions Import
 
-To cancel the effect of the option, use instead ``Unset Automatic Coercions Import``.
+   Since |Coq| version 8.3, the coercions present in a module are activated
+   only when the module is explicitly imported. Formerly, the coercions
+   were activated as soon as the module was required, whatever it was
+   imported or not.
 
+   This option makes it possible to recover the behavior of the versions of
+   |Coq| prior to 8.3.
 
 Examples
 --------
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 8861cac8a..d6955b310 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -466,80 +466,72 @@ Typeclasses Transparent, Typclasses Opaque
 This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
 
 
-Set Typeclasses Dependency Order
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+.. opt:: Typeclasses Dependency Order
 
-This option (on by default since 8.6) respects the dependency order
-between subgoals, meaning that subgoals which are depended on by other
-subgoals come first, while the non-dependent subgoals were put before
-the dependent ones previously (Coq v8.5 and below). This can result in
-quite different performance behaviors of proof search.
+   This option (on by default since 8.6) respects the dependency order
+   between subgoals, meaning that subgoals which are depended on by other
+   subgoals come first, while the non-dependent subgoals were put before
+   the dependent ones previously (Coq v8.5 and below). This can result in
+   quite different performance behaviors of proof search.
 
 
-Set Typeclasses Filtered Unification
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+.. opt:: Typeclasses Filtered Unification
 
-This option, available since Coq 8.6 and off by default, switches the
-hint application procedure to a filter-then-unify strategy. To apply a
-hint, we first check that the goal *matches* syntactically the
-inferred or specified pattern of the hint, and only then try to
-*unify* the goal with the conclusion of the hint. This can drastically
-improve performance by calling unification less often, matching
-syntactic patterns being very quick. This also provides more control
-on the triggering of instances. For example, forcing a constant to
-explicitely appear in the pattern will make it never apply on a goal
-where there is a hole in that place.
+   This option, available since Coq 8.6 and off by default, switches the
+   hint application procedure to a filter-then-unify strategy. To apply a
+   hint, we first check that the goal *matches* syntactically the
+   inferred or specified pattern of the hint, and only then try to
+   *unify* the goal with the conclusion of the hint. This can drastically
+   improve performance by calling unification less often, matching
+   syntactic patterns being very quick. This also provides more control
+   on the triggering of instances. For example, forcing a constant to
+   explicitely appear in the pattern will make it never apply on a goal
+   where there is a hole in that place.
 
 
-Set Typeclasses Limit Intros
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+.. opt:: Typeclasses Limit Intros
 
+   This option (on by default) controls the ability to apply hints while
+   avoiding (functional) eta-expansions in the generated proof term. It
+   does so by allowing hints that conclude in a product to apply to a
+   goal with a matching product directly, avoiding an introduction.
+   *Warning:* this can be expensive as it requires rebuilding hint
+   clauses dynamically, and does not benefit from the invertibility
+   status of the product introduction rule, resulting in potentially more
+   expensive proof-search (i.e. more useless backtracking).
 
-This option (on by default) controls the ability to apply hints while
-avoiding (functional) eta-expansions in the generated proof term. It
-does so by allowing hints that conclude in a product to apply to a
-goal with a matching product directly, avoiding an introduction.
-*Warning:* this can be expensive as it requires rebuilding hint
-clauses dynamically, and does not benefit from the invertibility
-status of the product introduction rule, resulting in potentially more
-expensive proof-search (i.e. more useless backtracking).
 
+.. opt:: Typeclass Resolution For Conversion
 
-Set Typeclass Resolution For Conversion
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   This option (on by default) controls the use of typeclass resolution
+   when a unification problem cannot be solved during elaboration/type-
+   inference. With this option on, when a unification fails, typeclass
+   resolution is tried before launching unification once again.
 
-This option (on by default) controls the use of typeclass resolution
-when a unification problem cannot be solved during elaboration/type-
-inference. With this option on, when a unification fails, typeclass
-resolution is tried before launching unification once again.
 
+.. opt:: Typeclasses Strict Resolution
 
-Set Typeclasses Strict Resolution
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   Typeclass declarations introduced when this option is set have a
+   stricter resolution behavior (the option is off by default). When
+   looking for unifications of a goal with an instance of this class, we
+   “freeze” all the existentials appearing in the goals, meaning that
+   they are considered rigid during unification and cannot be
+   instantiated.
 
-Typeclass declarations introduced when this option is set have a
-stricter resolution behavior (the option is off by default). When
-looking for unifications of a goal with an instance of this class, we
-“freeze” all the existentials appearing in the goals, meaning that
-they are considered rigid during unification and cannot be
-instantiated.
 
+.. opt:: Typeclasses Unique Solutions
 
-Set Typeclasses Unique Solutions
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+   When a typeclass resolution is launched we ensure that it has a single
+   solution or fail. This ensures that the resolution is canonical, but
+   can make proof search much more expensive.
 
-When a typeclass resolution is launched we ensure that it has a single
-solution or fail. This ensures that the resolution is canonical, but
-can make proof search much more expensive.
 
+.. opt:: Typeclasses Unique Instances
 
-Set Typeclasses Unique Instances
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Typeclass declarations introduced when this option is set have a more
-efficient resolution behavior (the option is off by default). When a
-solution to the typeclass goal of this class is found, we never
-backtrack on it, assuming that it is canonical.
+   Typeclass declarations introduced when this option is set have a more
+   efficient resolution behavior (the option is off by default). When a
+   solution to the typeclass goal of this class is found, we never
+   backtrack on it, assuming that it is canonical.
 
 
 Typeclasses eauto `:=`
@@ -562,7 +554,7 @@ Typeclasses eauto `:=`
 Set Typeclasses Debug
 ~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Set Typeclasses Debug {? Verbosity @num}
+.. opt:: Typeclasses Debug {? Verbosity @num}
 
 These options allow to see the resolution steps of typeclasses that are
 performed during search. The ``Debug`` option is synonymous to ``Debug
@@ -570,11 +562,10 @@ Verbosity 1``, and ``Debug Verbosity 2`` provides more information
 (tried tactics, shelving of goals, etc…).
 
 
-Set Refine Instance Mode
-~~~~~~~~~~~~~~~~~~~~~~~~
+.. opt:: Refine Instance Mode
 
-The option Refine Instance Mode allows to switch the behavior of
-instance declarations made through the Instance command.
+This options allows to switch the behavior of instance declarations made through
+the Instance command.
 
 + When it is on (the default), instances that have unsolved holes in
   their proof-term silently open the proof mode with the remaining
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index f474eade7..8d47949db 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -148,7 +148,7 @@ available:
 
 It can be activated for printing with
 
-.. cmd:: Set Printing Projections.
+.. opt:: Printing Projections
 
 .. example::
 
@@ -249,7 +249,7 @@ printing of pattern-matching over primitive records.
 Primitive Record Types
 ++++++++++++++++++++++
 
-When the ``Set Primitive Projections`` option is on, definitions of
+When the :opt:`Primitive Projections` option is on, definitions of
 record types change meaning. When a type is declared with primitive
 projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though).
 To eliminate the (co-)inductive type, one must use its defined primitive projections.
@@ -328,7 +328,7 @@ patterns are allowed, as in ML-like languages.
 The extension just acts as a macro that is expanded during parsing
 into a sequence of match on simple patterns. Especially, a
 construction defined using the extended match is generally printed
-under its expanded form (see ``Set Printing Matching`` in :ref:`controlling-match-pp`).
+under its expanded form (see :opt:`Printing Matching`).
 
 See also: :ref:`extendedpatternmatching`.
 
@@ -1506,10 +1506,10 @@ inserted. In the second case, the function is considered to be
 implicitly applied to the implicit arguments it is waiting for: one
 says that the implicit argument is maximally inserted.
 
-Each implicit argument can be declared to have to be inserted
-maximally or non maximally. This can be governed argument per argument
-by the command ``Implicit Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the
-command ``Set Maximal Implicit Insertion`` (see Section :ref:`controlling-insertion-implicit-args`).
+Each implicit argument can be declared to have to be inserted maximally or non
+maximally. This can be governed argument per argument by the command ``Implicit
+Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the
+:opt:`Maximal Implicit Insertion` option.
 See also :ref:`displaying-implicit-args`.
 
 
@@ -1882,7 +1882,7 @@ arguments that are not detected as strict implicit arguments. This
 “defensive” mode can quickly make the display cumbersome so this can
 be deactivated by turning this option off.
 
-See also: ``Set Printing All`` in :ref:`printing_constructions_full`.
+See also: :opt:`Printing All`.
 
 Interaction with subtyping
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2134,9 +2134,9 @@ sensitive to the implicit arguments). Turning this option on
 deactivates all high-level printing features such as coercions,
 implicit arguments, returned type of pattern-matching, notations and
 various syntactic sugar for pattern-matching or record projections.
-Otherwise said, ``Set Printing All`` includes the effects of the commands
-``Set Printing Implicit``, ``Set Printing Coercions``, ``Set Printing Synth``,
-``Unset Printing Projections``, and ``Unset Printing Notations``. To reactivate
+Otherwise said, :opt:`Printing All` includes the effects of the options
+:opt:`Printing Implicit`, :opt:`Printing Coercions`, :opt:`Printing Synth`,
+:opt:`Printing Projections`, and :opt:`Printing Notations`. To reactivate
 the high-level printing features, use the command ``Unset Printing All``.
 
 .. _printing-universes:
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 074c6f1e2..6ddb0b027 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2749,12 +2749,9 @@ type classes inference.
   No inference for ``t``. Unresolved instances are
   quantified in the (inferred) type of ``t`` and abstracted in ``t``.
 
+.. opt:: SsrHave NoTCResolution
 
-The behavior of |SSR| 1.4 and below (never resolve type classes)
-can be restored with the option
-
-.. cmd:: Set SsrHave NoTCResolution.
-
+   This option restores the behavior of |SSR| 1.4 and below (never resolve type classes).
 
 Variants: the suff and wlog tactics
 ```````````````````````````````````
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 08aa7110d..1868f4b9d 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -51,20 +51,15 @@ specified, the default selector is used.
      tactic_invocation : toplevel_selector : tactic.
                        : |tactic .
 
-.. cmd:: Set Default Goal Selector @toplevel_selector.
+.. opt:: Default Goal Selector @toplevel_selector.
 
-After using this command, the default selector – used when no selector
-is specified when applying a tactic – is set to the chosen value. The
-initial value is 1, hence the tactics are, by default, applied to the
-first goal. Using Set Default Goal Selector ‘‘all’’ will make is so
-that tactics are, by default, applied to every goal simultaneously.
-Then, to apply a tactic tac to the first goal only, you can write
-1:tac. Although more selectors are available, only ‘‘all’’ or a single
-natural number are valid default goal selectors.
-
-.. cmd:: Test Default Goal Selector.
-
-This command displays the current default selector.
+   This option controls the default selector – used when no selector is
+   specified when applying a tactic – is set to the chosen value. The initial
+   value is 1, hence the tactics are, by default, applied to the first goal.
+   Using value ``all`` will make is so that tactics are, by default, applied to
+   every goal simultaneously. Then, to apply a tactic tac to the first goal
+   only, you can write ``1:tac``. Although more selectors are available, only
+   ``all`` or a single natural number are valid default goal selectors.
 
 .. _bindingslist:
 
@@ -123,14 +118,12 @@ following syntax:
 
 The role of an occurrence clause is to select a set of occurrences of a term in
 a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that
-occurrences have to be selected in the hypotheses named :n:`@ident`. If no numbers
-are given for hypothesis :n:`@ident`, then all the occurrences of `term` in the
-hypothesis are selected. If numbers are given, they refer to occurrences of
-`term` when the term is printed using option ``Set Printing All`` (see
-:ref:`printing_constructions_full`), counting from left to right. In
-particular, occurrences of `term` in implicit arguments (see
-:ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`)
-are counted.
+occurrences have to be selected in the hypotheses named :n:`@ident`. If no
+numbers are given for hypothesis :n:`@ident`, then all the occurrences of `term`
+in the hypothesis are selected. If numbers are given, they refer to occurrences
+of `term` when the term is printed using option :opt:`Printing All`, counting
+from left to right. In particular, occurrences of `term` in implicit arguments
+(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted.
 
 If a minus sign is given between at and the list of occurrences, it
 negates the condition so that the clause denotes all the occurrences
@@ -346,7 +339,7 @@ does.
 This summarizes the different syntaxes for ``apply`` and ``eapply``.
 
 .. tacv:: lapply @term
-   :name: `lapply
+   :name: lapply
 
 This tactic applies to any goal, say :g:`G`. The argument term has to be
 well-formed in the current context, its type being reducible to a non-dependent
@@ -437,7 +430,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by
    setting the following option:
 
-.. opt:: Set Universal Lemma Under Conjunction.
+.. opt:: Universal Lemma Under Conjunction
 
    This option, which preserves compatibility with versions of Coq prior to
    8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`).
@@ -829,15 +822,10 @@ quantification or an implication.
    so that all the arguments of the i-th constructors of the corresponding
    inductive type are introduced can be controlled with the following option:
 
-   .. cmd:: Set Bracketing Last Introduction Pattern.
-
-   Force completion, if needed, when the last introduction pattern is a
-   disjunctive or conjunctive pattern (this is the default).
+   .. opt:: Bracketing Last Introduction Pattern
 
-   .. cmd:: Unset Bracketing Last Introduction Pattern.
-
-   Deactivate completion when the last introduction pattern is a disjunctive or
-   conjunctive pattern.
+      Force completion, if needed, when the last introduction pattern is a
+      disjunctive or conjunctive pattern (on by default).
 
 .. tacn:: clear @ident
    :name: clear
@@ -1239,7 +1227,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
 
    This is equivalent to :n:`generalize @term` but it generalizes only over the
    specified occurrences of :n:`@term` (counting from left to right on the
-   expression printed using option :g:`Set Printing All`).
+   expression printed using option :opt:`Printing All`).
 
 .. tacv:: generalize @term as @ident
 
@@ -1964,13 +1952,13 @@ It is possible to ensure that :n:`injection @term` erases the original
 hypothesis and leaves the generated equalities in the context rather
 than putting them as antecedents of the current goal, as if giving
 :n:`injection @term as` (with an empty list of names). To obtain this
-behavior, the option ``Set Structural Injection`` must be activated. This
+behavior, the option :opt:`Structural Injection` must be activated. This
 option is off by default.
 
-By default, ``injection`` only creates new equalities between :n:`@terms` whose
+By default, :tacn:`injection` only creates new equalities between :n:`@terms` whose
 type is in sort :g:`Type` or :g:`Set`, thus implementing a special behavior for
 objects that are proofs of a statement in :g:`Prop`. This behavior can be
-turned off by setting the option ``Set Keep Proof Equalities``.
+turned off by setting the option :opt:`Keep Proof Equalities`.
 
 .. tacn:: inversion @ident
    :name: inversion
@@ -1996,8 +1984,8 @@ turned off by setting the option ``Set Keep Proof Equalities``.
    equalities between expressions that appeared in the hypothesis that is
    being processed. By default, no equalities are generated if they
    relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort
-   :g:`Prop`). This behavior can be turned off by using the option ``Set Keep
-   Proof Equalities``.
+   :g:`Prop`). This behavior can be turned off by using the option
+   :opt`Keep Proof Equalities`.
 
 .. tacv:: inversion @num
 
@@ -2513,28 +2501,28 @@ unfolded and cleared.
 
      ..  note::
 
-       The behavior of subst can be controlled using option ``Set Regular Subst
-       Tactic.`` When this option is activated, subst also deals with the
-       following corner cases:
-
-        + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2`
-          and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not
-          a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u`
-          or :n:`u = @ident`:sub:`2`; without the option, a second call to
-          subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or
-          `t′` respectively.
-        + The presence of a recursive equation which without the option would
-          be a cause of failure of :tacn:`subst`.
-        + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2`
-          and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the
-          option would be a cause of failure of :tacn:`subst`.
-
-       Additionally, it prevents a local definition such as :n:`@ident := t` to be
-       unfolded which otherwise it would exceptionally unfold in configurations
-       containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident`
-       with `u′` not a variable. Finally, it preserves the initial order of
-       hypotheses, which without the option it may break. The option is on by
-       default.
+         The behavior of subst can be controlled using option :opt:`Regular Subst
+         Tactic`. When this option is activated, subst also deals with the
+         following corner cases:
+
+         + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2`
+           and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not
+           a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u`
+           or :n:`u = @ident`:sub:`2`; without the option, a second call to
+           subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or
+           `t′` respectively.
+         + The presence of a recursive equation which without the option would
+           be a cause of failure of :tacn:`subst`.
+         + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2`
+           and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the
+           option would be a cause of failure of :tacn:`subst`.
+
+         Additionally, it prevents a local definition such as :n:`@ident := t` to be
+         unfolded which otherwise it would exceptionally unfold in configurations
+         containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident`
+         with `u′` not a variable. Finally, it preserves the initial order of
+         hypotheses, which without the option it may break. The option is on by
+         default.
 
 
 .. tacn:: stepl @term
@@ -3578,24 +3566,21 @@ We propose a smooth transitional path by providing the ``Loose Hint Behavior``
 option which accepts three flags allowing for a fine-grained handling of
 non-imported hints.
 
-**Variants:**
-
-.. cmd:: Set Loose Hint Behavior "Lax"
+.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %)
 
-   This is the default, and corresponds to the historical behavior, that
-   is, hints defined outside of a section have a global scope.
+   This option accepts three values, which control the behavior of hints w.r.t.
+   :cmd:`Import`:
 
-.. cmd:: Set Loose Hint Behavior "Warn"
+   - "Lax": this is the default, and corresponds to the historical behavior,
+     that is, hints defined outside of a section have a global scope.
 
-   When set, it outputs a warning when a non-imported hint is used. Note that
-   this is an over-approximation, because a hint may be triggered by a run that
-   will eventually fail and backtrack, resulting in the hint not being actually
-   useful for the proof.
+   - "Warn": outputs a warning when a non-imported hint is used. Note that this
+     is an over-approximation, because a hint may be triggered by a run that
+     will eventually fail and backtrack, resulting in the hint not being
+     actually useful for the proof.
 
-.. cmd:: Set Loose Hint Behavior "Strict"
-
-   When set, it changes the behavior of an unloaded hint to a immediate fail
-   tactic, allowing to emulate an import-scoped hint mechanism.
+   - "Strict": changes the behavior of an unloaded hint to a immediate fail
+     tactic, allowing to emulate an import-scoped hint mechanism.
 
 .. _tactics-implicit-automation:
 
@@ -3734,17 +3719,10 @@ some incompatibilities.
   Empty_set, unit, True``, :tacn:`dintuition` recognizes also all inductive
   types with one constructors and no indices, i.e. record-style connectives.
 
-Some aspects of the tactic :tacn:`intuition` can be controlled using options.
-To avoid that inner negations which do not need to be unfolded are
-unfolded, use:
-
-.. cmd:: Unset Intuition Negation Unfolding
-
+.. opt:: Intuition Negation Unfolding
 
-To do that all negations of the goal are unfolded even inner ones
-(this is the default), use:
-
-.. cmd:: Set Intuition Negation Unfolding
+   Controls whether :tacn:`intuition` unfolds inner negations which do not need
+   to be unfolded. This option is on by default.
 
 .. tacn:: rtauto
    :name: rtauto
@@ -3769,9 +3747,8 @@ usual logical connectives but instead may reason about any first-order class
 inductive definition.
 
 The default tactic used by :tacn:`firstorder` when no rule applies is :g:`auto
-with \*`, it can be reset locally or globally using the ``Set Firstorder
-Solver`` tactic vernacular command and printed using ``Print Firstorder
-Solver``.
+with \*`, it can be reset locally or globally using the :opt:`Firstorder Solver`
+option and printed using :cmd:`Print Firstorder Solver`.
 
 .. tacv:: firstorder @tactic
 
@@ -3792,8 +3769,9 @@ Solver``.
 
   This combines the effects of the different variants of :tacn:`firstorder`.
 
-Proof-search is bounded by a depth parameter which can be set by
-typing the ``Set Firstorder Depth n`` vernacular command.
+.. opt:: Firstorder Depth @natural
+
+   This option controls the proof-search depth bound.
 
 .. tacn:: congruence
    :name: congruence
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 8abff303c..6b3600040 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -77,14 +77,11 @@ section.
 Flags, Options and Tables
 -----------------------------
 
-|Coq| configurability is based on flags (e.g. ``Set Printing All`` in
-Section :ref:`printing_constructions_full`), options (e.g. ``Set Printing Widthinteger`` in Section
-:ref:`controlling-display`), or tables (e.g. ``Add Printing Record ident``, in Section
-:ref:`record-types`).
-The names of flags, options and tables are made of non-empty sequences of identifiers
-(conventionally with capital initial
-letter). The general commands handling flags, options and tables are
-given below.
+|Coq| configurability is based on flags (e.g. :opt:`Printing All`), options
+(e.g. :opt:`Printing Width`), or tables (e.g. :cmd:`Add Printing Record`). The
+names of flags, options and tables are made of non-empty sequences of
+identifiers (conventionally with capital initial letter). The general commands
+handling flags, options and tables are given below.
 
 .. TODO : flag is not a syntax entry
 
@@ -93,7 +90,6 @@ given below.
 This command switches :n:`@flag` on. The original state of :n:`@flag` is restored
 when the current module ends.
 
-
 Variants:
 
 .. cmdv:: Local Set @flag.
@@ -274,11 +270,10 @@ See also: Section :ref:`performingcomputations`.
 .. cmd::Extraction @term.
 
 This command displays the extracted term from :n:`@term`. The extraction is
-processed according to the distinction between ``Set`` and ``Prop``; that is
-to say, between logical and computational content (see Section
-:ref:`sorts`). The extracted term is displayed in OCaml
-syntax,
-where global identifiers are still displayed as in |Coq| terms.
+processed according to the distinction between :g:`Set` and :g:`Prop`; that is
+to say, between logical and computational content (see Section :ref:`sorts`).
+The extracted term is displayed in OCaml syntax, where global identifiers are
+still displayed as in |Coq| terms.
 
 
 Variants:
@@ -1083,20 +1078,11 @@ expressed in seconds), then it is interrupted and an error message is
 displayed.
 
 
-.. cmd:: Set Default Timeout @num.
-
-After using this command, all subsequent commands behave as if they
-were passed to a Timeout command. Commands already starting by a
-`Timeout` are unaffected.
-
-
-.. cmd:: Unset Default Timeout.
-
-This command turns off the use of a default timeout.
-
-.. cmd:: Test Default Timeout.
+.. opt:: Default Timeout @num
 
-This command displays whether some default timeout has been set or not.
+   This option controls a default timeout for subsequent commands, as if they
+   were passed to a :cmd:`Timeout` command. Commands already starting by a
+   :cmd:`Timeout` are unaffected.
 
 .. cmd:: Fail @command.
 
@@ -1117,128 +1103,58 @@ Error messages:
 Controlling display
 -----------------------
 
+.. opt:: Silent
 
-.. cmd:: Set Silent.
-
-This command turns off the normal displaying.
-
-
-.. cmd:: Unset Silent.
-
-This command turns the normal display on.
-
-.. todo:: check that spaces are handled well
-
-.. cmd:: Set Warnings ‘‘(@ident {* , @ident } )’’.
-
-This command configures the display of warnings. It is experimental,
-and expects, between quotes, a comma-separated list of warning names
-or categories. Adding - in front of a warning or category disables it,
-adding + makes it an error. It is possible to use the special
-categories all and default, the latter containing the warnings enabled
-by default. The flags are interpreted from left to right, so in case
-of an overlap, the flags on the right have higher priority, meaning
-that `A,-A` is equivalent to `-A`.
-
-
-.. cmd:: Set Search Output Name Only.
-
-This command restricts the output of search commands to identifier
-names; turning it on causes invocations of ``Search``, ``SearchHead``,
-``SearchPattern``, ``SearchRewrite`` etc. to omit types from their output,
-printing only identifiers.
-
-
-.. cmd:: Unset Search Output Name Only.
-
-This command turns type display in search results back on.
-
-
-.. cmd:: Set Printing Width @integer.
-
-This command sets which left-aligned part of the width of the screen
-is used for display.
-
-
-.. cmd:: Unset Printing Width.
-
-This command resets the width of the screen used for display to its
-default value (which is 78 at the time of writing this documentation).
-
-
-.. cmd:: Test Printing Width.
-
-This command displays the current screen width used for display.
-
-
-.. cmd:: Set Printing Depth @integer.
-
-This command sets the nesting depth of the formatter used for pretty-
-printing. Beyond this depth, display of subterms is replaced by dots.
-
-
-.. cmd:: Unset Printing Depth.
-
-This command resets the nesting depth of the formatter used for
-pretty-printing to its default value (at the time of writing this
-documentation, the default value is 50).
-
-
-.. cmd:: Test Printing Depth.
-
-This command displays the current nesting depth used for display.
-
-
-.. cmd:: Unset Printing Compact Contexts.
-
-This command resets the displaying of goals contexts to non compact
-mode (default at the time of writing this documentation). Non compact
-means that consecutive variables of different types are printed on
-different lines.
-
-
-.. cmd:: Set Printing Compact Contexts.
-
-This command sets the displaying of goals contexts to compact mode.
-The printer tries to reduce the vertical size of goals contexts by
-putting several variables (even if of different types) on the same
-line provided it does not exceed the printing width (See Set Printing
-Width above).
-
-
-.. cmd:: Test Printing Compact Contexts.
-
-This command displays the current state of compaction of goal.
+   This option controls the normal displaying.
 
+.. opt:: Warnings "@ident {* , @ident }"
 
-.. cmd:: Unset Printing Unfocused.
+   This option configures the display of warnings. It is experimental, and
+   expects, between quotes, a comma-separated list of warning names or
+   categories. Adding - in front of a warning or category disables it, adding +
+   makes it an error. It is possible to use the special categories all and
+   default, the latter containing the warnings enabled by default. The flags are
+   interpreted from left to right, so in case of an overlap, the flags on the
+   right have higher priority, meaning that `A,-A` is equivalent to `-A`.
 
-This command resets the displaying of goals to focused goals only
-(default). Unfocused goals are created by focusing other goals with
-bullets (see :ref:`bullets`) or curly braces (see `here <curly-braces>`).
+.. opt:: Search Output Name Only
 
+   This option restricts the output of search commands to identifier names;
+   turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`,
+   :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their
+   output, printing only identifiers.
 
-.. cmd:: Set Printing Unfocused.
+.. opt:: Printing Width @integer
 
-This command enables the displaying of unfocused goals. The goals are
-displayed after the focused ones and are distinguished by a separator.
+   This command sets which left-aligned part of the width of the screen is used
+   for display. At the time of writing this documentation, the default value
+   is 78.
 
+.. opt:: Printing Depth @integer
 
-.. cmd:: Test Printing Unfocused.
+   This option controls the nesting depth of the formatter used for pretty-
+   printing. Beyond this depth, display of subterms is replaced by dots. At the
+   time of writing this documentation, the default value is 50.
 
-This command displays the current state of unfocused goals display.
+.. opt:: Printing Compact Contexts
 
+   This option controls the compact display mode for goals contexts. When on,
+   the printer tries to reduce the vertical size of goals contexts by putting
+   several variables (even if of different types) on the same line provided it
+   does not exceed the printing width (see :opt:`Printing Width`). At the time
+   of writing this documentation, it is off by default.
 
-.. cmd:: Set Printing Dependent Evars Line.
+.. opt:: Printing Unfocused
 
-This command enables the printing of the “(dependent evars: …)” line
-when -emacs is passed.
+   This option controls whether unfocused goals are displayed. Such goals are
+   created by focusing other goals with bullets (see :ref:`bullets`) or curly
+   braces (see `here <curly-braces>`). It is off by default.
 
+.. cmd:: Printing Dependent Evars Line
 
-.. cmd:: Unset Printing Dependent Evars Line.
+   This option controls the printing of the “(dependent evars: …)” line when
+   ``-emacs`` is passed.
 
-This command disables the printing of the “(dependent evars: …)” line
-when -emacs is passed.
 
 .. _vernac-controlling-the-reduction-strategies: