Clean-up around options.

- Remove all trailing dots.
- There is only one Bullet Behavior option.
- Replaces `@natural` and `@integer` by `@num`.

7 files changed, 36 insertions, 41 deletions

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 3d8d9087d1..75d7972019 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -46,7 +46,7 @@ the expressiveness of the theory remains the same. Once the stage of
 parsing has finished only simple patterns remain. Re-nesting of
 pattern is performed at printing time. An easy way to see the result
 of the expansion is to toggle off the nesting performed at printing
-(use here :opt:`Set Printing Matching`), then by printing the term with :cmd:`Print`
+(use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print`
 if the term is a constant, or using the command :cmd:`Check`.
 
 The extended ``match`` still accepts an optional *elimination predicate*
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 38365e4035..97963dbafe 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -131,14 +131,14 @@ order to produce more readable code.
 
 The type-preserving optimizations are controlled by the following |Coq| options:
 
-.. opt:: Extraction Optimize.
+.. opt:: Extraction Optimize
 
    Default is on. This controls all type-preserving optimizations made on
    the ML terms (mostly reduction of dummy beta/iota redexes, but also
    simplifications on Cases, etc). Turn this option off if you want a
    ML term as close as possible to the Coq term.
 
-.. opt:: Extraction Conservative Types.
+.. opt:: Extraction Conservative Types
 
    Default is off. This controls the non type-preserving optimizations
    made on ML terms (which try to avoid function abstraction of dummy
@@ -146,7 +146,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted
    code of ``e`` and ``t`` respectively.
 
-.. opt:: Extraction KeepSingleton.
+.. opt:: Extraction KeepSingleton
 
    Default is off. Normally, when the extraction of an inductive type
    produces a singleton type (i.e. a type with only one constructor, and
@@ -155,7 +155,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    The typical example is ``sig``. This option allows disabling this
    optimization when one wishes to preserve the inductive structure of types.
 
-.. opt:: Extraction AutoInline.
+.. opt:: Extraction AutoInline
 
    Default is on. The extraction mechanism inlines the bodies of
    some defined constants, according to some heuristics
@@ -227,7 +227,7 @@ When an actual extraction takes place, an error is normally raised if the
 if any of the implicited variables still occurs in the final code.
 This behavior can be relaxed via the following option:
 
-.. opt:: Extraction SafeImplicits.
+.. opt:: Extraction SafeImplicits
 
    Default is on. When this option is off, a warning is emitted
    instead of an error if some implicited variables still occur in the
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index a93e9b156d..d6bbcd37ea 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -475,7 +475,7 @@ of :g:`match` expressions.
 Printing nested patterns
 +++++++++++++++++++++++++
 
-.. opt:: Printing Matching.
+.. opt:: Printing Matching
 
 The Calculus of Inductive Constructions knows pattern-matching only
 over simple patterns. It is however convenient to re-factorize nested
@@ -491,7 +491,7 @@ in the same way as the |Coq| kernel handles them.
 Factorization of clauses with same right-hand side
 ++++++++++++++++++++++++++++++++++++++++++++++++++
 
-.. opt:: Printing Factorizable Match Patterns.
+.. opt:: Printing Factorizable Match Patterns
 
 When several patterns share the same right-hand side, it is additionally
 possible to share the clauses using disjunctive patterns. Assuming that the
@@ -501,7 +501,7 @@ printer to try to do this kind of factorization.
 Use of a default clause
 +++++++++++++++++++++++
 
-.. opt:: Printing Allow Default Clause.
+.. opt:: Printing Allow Default Clause
 
 When several patterns share the same right-hand side which do not depend on the
 arguments of the patterns, yet an extra factorization is possible: the
@@ -512,7 +512,7 @@ default) tells |Coq|'s printer to use a default clause when relevant.
 Printing of wildcard patterns
 ++++++++++++++++++++++++++++++
 
-.. opt:: Printing Wildcard.
+.. opt:: Printing Wildcard
 
 Some variables in a pattern may not occur in the right-hand side of
 the pattern-matching clause. When this option is on (default), the
@@ -524,7 +524,7 @@ pattern-matching clause are just printed using the wildcard symbol
 Printing of the elimination predicate
 +++++++++++++++++++++++++++++++++++++
 
-.. opt:: Printing Synth.
+.. opt:: Printing Synth
 
 In most of the cases, the type of the result of a matched term is
 mechanically synthesizable. Especially, if the result type does not
@@ -1742,7 +1742,7 @@ appear strictly in the body of the type, they are implicit.
 Mode for automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Implicit Arguments.
+.. opt:: Implicit Arguments
 
 This option (off by default) allows to systematically declare implicit
 the arguments detectable as such. Auto-detection of implicit arguments is
@@ -1754,7 +1754,7 @@ arguments have to be considered or not.
 Controlling strict implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Strict Implicit.
+.. opt:: Strict Implicit
 
 When the mode for automatic declaration of implicit arguments is on,
 the default is to automatically set implicit only the strict implicit
@@ -1763,7 +1763,7 @@ implicit arguments. To relax this constraint and to set
 implicit all non strict implicit arguments by default, you can turn this
 option off.
 
-.. opt:: Strongly Strict Implicit.
+.. opt:: Strongly Strict Implicit
 
 Use this option (off by default) to capture exactly the strict implicit
 arguments and no more than the strict implicit arguments.
@@ -1773,7 +1773,7 @@ arguments and no more than the strict implicit arguments.
 Controlling contextual implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Contextual Implicit.
+.. opt:: Contextual Implicit
 
 By default, |Coq| does not automatically set implicit the contextual
 implicit arguments. You can turn this option on to tell |Coq| to also
@@ -1784,7 +1784,7 @@ infer contextual implicit argument.
 Controlling reversible-pattern implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Reversible Pattern Implicit.
+.. opt:: Reversible Pattern Implicit
 
 By default, |Coq| does not automatically set implicit the reversible-pattern
 implicit arguments. You can turn this option on to tell |Coq| to also infer
@@ -1795,7 +1795,7 @@ reversible-pattern implicit argument.
 Controlling the insertion of implicit arguments not followed by explicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Maximal Implicit Insertion.
+.. opt:: Maximal Implicit Insertion
 
 Assuming the implicit argument mode is on, this option (off by default)
 declares implicit arguments to be automatically inserted when a
@@ -1867,18 +1867,18 @@ Displaying what the implicit arguments are
 To display the implicit arguments associated to an object, and to know
 if each of them is to be used maximally or not, use the command
 
-.. cmd:: Print Implicit @qualid.
+.. cmd:: Print Implicit @qualid
 
 Explicit displaying of implicit arguments for pretty-printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Printing Implicit.
+.. opt:: Printing Implicit
 
 By default, the basic pretty-printing rules hide the inferable implicit
 arguments of an application. Turn this option on to force printing all
 implicit arguments.
 
-.. opt:: Printing Implicit Defensive.
+.. opt:: Printing Implicit Defensive
 
 By default, the basic pretty-printing rules display the implicit
 arguments that are not detected as strict implicit arguments. This
@@ -1910,9 +1910,9 @@ but succeeds in
 Deactivation of implicit arguments for parsing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Parsing Explicit.
+.. opt:: Parsing Explicit
 
-Turning this option on, deactivates the use of implicit arguments.
+Turning this option on (it is off by default) deactivates the use of implicit arguments.
 
 In this case, all arguments of constants, inductive types,
 constructors, etc, including the arguments declared as implicit, have
@@ -2128,7 +2128,7 @@ to coercions are provided in :ref:`implicitcoercions`.
 Printing constructions in full
 ------------------------------
 
-.. opt:: Printing All.
+.. opt:: Printing All
 
 Coercions, implicit arguments, the type of pattern-matching, but also
 notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some
@@ -2147,7 +2147,7 @@ the high-level printing features, use the command ``Unset Printing All``.
 Printing universes
 ------------------
 
-.. opt:: Printing Universes.
+.. opt:: Printing Universes
 
 Turn this option on to activate the display of the actual level of each
 occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in
@@ -2237,7 +2237,7 @@ with a named-goal selector, see :ref:`goal-selectors`).
 Explicit displaying of existential instances for pretty-printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Printing Existential Instances.
+.. opt:: Printing Existential Instances
 
 This option (off by default) activates the full display of how the
 context of an existential variable is instantiated at each of the
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index b70c79f689..2d08acc402 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1147,7 +1147,7 @@ Info trace
    script. In particular, the calls to idtac in branches which failed are
    not printed.
 
-   .. opt:: Info Level @num.
+   .. opt:: Info Level @num
 
       This option is an alternative to the ``Info`` command.
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 64e28cea43..53205b6193 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -95,7 +95,7 @@ has been opened using the ``Goal`` command.
 .. cmd:: Admitted.
    :name: Admitted (interactive proof)
 
-This command is available in interactive editing proof mode to give up
+This command is available in interactive editing mode to give up
 the current proof and declare the initial goal as an axiom.
 
 .. cmd:: Proof @term.
@@ -185,14 +185,14 @@ Proof using options
 The following options modify the behavior of ``Proof using``.
 
 
-.. opt:: Default Proof Using "@expression".
+.. opt:: Default Proof Using "@expression"
 
    Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default
    Proof Using "a b"``. will complete all ``Proof`` commands not followed by a
    using part with using ``a`` ``b``.
 
 
-.. opt:: Suggest Proof Using.
+.. opt:: Suggest Proof Using
 
    When ``Qed`` is performed, suggest a using annotation if the user did not
    provide one.
@@ -427,17 +427,12 @@ You just finished a goal focused by ``{``, you must unfocus it with ``}``.
 
 Set Bullet Behavior
 ```````````````````
+.. opt:: Bullet Behavior  %( "None" %| "Strict Subproofs" %)
 
-The bullet behavior can be controlled by the following commands.
-
-.. opt:: Bullet Behavior "None"
-
-This makes bullets inactive.
-
-.. opt:: Bullet Behavior "Strict Subproofs"
-
-This makes bullets active (this is the default behavior).
+   This option controls the bullet behavior and can take two possible values:
 
+   - "None": this makes bullets inactive.
+   - "Strict Subproofs": this makes bullets active (this is the default behavior).
 
 .. _requestinginformation:
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 5673b496e6..526a7d3bf3 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3860,7 +3860,7 @@ inductive definition.
 
   This combines the effects of the different variants of :tacn:`firstorder`.
 
-.. opt:: Firstorder Depth @natural
+.. opt:: Firstorder Depth @num
 
    This option controls the proof-search depth bound.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 692ff294a6..672c7a0fe1 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1131,13 +1131,13 @@ Controlling display
    :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their
    output, printing only identifiers.
 
-.. opt:: Printing Width @integer
+.. opt:: Printing Width @num
 
    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
+.. opt:: Printing Depth @num
 
    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