[Sphinx] Fix a lot of references and description of options

2 files changed, 68 insertions, 84 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