Rewrite "Flags, Options and Tables" section.

Mark boolean-valued options with :flag:
Adjust tactic and command names so parameters aren't shown in the index unless
they're needed for disambiguation.
Remove references to synchronous options.
Revise doc for tables.
Correct indentation for text below :flag:

1 files changed, 30 insertions, 24 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index b0b57d00a0..f99c539251 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -48,7 +48,8 @@ specified, the default selector is used.
      tactic_invocation : toplevel_selector : tactic.
                        : |tactic .
 
-.. opt:: Default Goal Selector @toplevel_selector
+.. opt:: Default Goal Selector "@toplevel_selector"
+   :name: Default Goal Selector
 
    This option controls the default selector, used when no selector is
    specified when applying a tactic. The initial value is 1, hence the
@@ -124,7 +125,7 @@ that occurrences have to be selected in the hypotheses named :token:`ident`.
 If no numbers are given for hypothesis :token:`ident`, then all the
 occurrences of :token:`term` in the hypothesis are selected. If numbers are
 given, they refer to occurrences of :token:`term` when the term is printed
-using option :opt:`Printing All`, counting from left to right. In particular,
+using option :flag:`Printing All`, counting from left to right. In particular,
 occurrences of :token:`term` in implicit arguments
 (see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are
 counted.
@@ -448,7 +449,7 @@ Applying theorems
    ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by
    setting the following option:
 
-.. opt:: Universal Lemma Under Conjunction
+.. flag:: 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`).
@@ -473,7 +474,7 @@ Applying theorems
    :token:`ident`. Tuples are decomposed in a width-first left-to-right order
    (for instance if the type of :g:`H1` is :g:`A <-> B` and the type of
    :g:`H2` is :g:`A` then :g:`apply H1 in H2` transforms the type of :g:`H2`
-   into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern-matching
+   into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern matching
    with dependent types.
 
    .. exn:: Statement without assumptions.
@@ -852,7 +853,7 @@ Managing the local context
    so that all the arguments of the i-th constructors of the corresponding
    inductive type are introduced can be controlled with the following option:
 
-   .. opt:: Bracketing Last Introduction Pattern
+   .. flag:: Bracketing Last Introduction Pattern
 
       Force completion, if needed, when the last introduction pattern is a
       disjunctive or conjunctive pattern (on by default).
@@ -1295,7 +1296,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 :opt:`Printing All`).
+   expression printed using option :flag:`Printing All`).
 
 .. tacv:: generalize @term as @ident
 
@@ -2038,14 +2039,14 @@ and an explanation of the underlying technique.
    to the number of new equalities. The original equality is erased if it
    corresponds to a hypothesis.
 
-   .. opt:: Structural Injection
+   .. flag:: Structural Injection
 
       This option 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). This option is off by default.
 
-   .. opt:: Keep Proof Equalities
+   .. flag:: Keep Proof Equalities
 
       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
@@ -2077,7 +2078,7 @@ and an explanation of the underlying technique.
    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
-   :opt`Keep Proof Equalities`.
+   :flag`Keep Proof Equalities`.
 
 .. tacv:: inversion @num
 
@@ -2587,7 +2588,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       context for which an equality of the form :n:`@ident = t` or :n:`t = @ident`
       or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``.
 
-   .. opt:: Regular Subst Tactic
+   .. flag:: Regular Subst Tactic
 
       This option controls the behavior of :tacn:`subst`. When it is
       activated (it is by default), :tacn:`subst` also deals with the following corner cases:
@@ -2722,7 +2723,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :math:`\beta` (reduction of functional application), :math:`\delta`
    (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`),
    :math:`\iota` (reduction of
-   pattern-matching over a constructed term, and unfolding of :g:`fix` and
+   pattern matching over a constructed term, and unfolding of :g:`fix` and
    :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the
    flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``,
    ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix``
@@ -2805,12 +2806,13 @@ the conversion in hypotheses :n:`{+ @ident}`.
    compilation cost is higher, so it is worth using only for intensive
    computations.
 
-   .. opt:: NativeCompute Profiling
+   .. flag:: NativeCompute Profiling
 
       On Linux, if you have the ``perf`` profiler installed, this option makes
       it possible to profile ``native_compute`` evaluations.
 
-   .. opt:: NativeCompute Profile Filename
+   .. opt:: NativeCompute Profile Filename @string
+      :name: NativeCompute Profile Filename
 
       This option specifies the profile output; the default is
       ``native_compute_profile.data``. The actual filename used
@@ -2821,7 +2823,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
       on the profile file to see the results. Consult the ``perf`` documentation
       for more details.
 
-.. opt:: Debug Cbv
+.. flag:: Debug Cbv
 
    This option makes :tacn:`cbv` (and its derivative :tacn:`compute`) print
    information about the constants it encounters and the unfolding decisions it
@@ -2988,7 +2990,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose
    head occurrence is :n:`@qualid` (or :n:`@string`).
 
-.. opt:: Debug RAKAM
+.. flag:: Debug RAKAM
 
    This option makes :tacn:`cbn` print various debugging information.
    ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine.
@@ -3195,10 +3197,11 @@ hints of the database named core.
 The following options enable printing of informative or debug information for
 the :tacn:`auto` and :tacn:`trivial` tactics:
 
-.. opt:: Info Auto
-.. opt:: Debug Auto
-.. opt:: Info Trivial
-.. opt:: Debug Trivial
+.. flag:: Info Auto
+          Debug Auto
+          Info Trivial
+          Debug Trivial
+   :undocumented:
 
 .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
@@ -3228,8 +3231,9 @@ Note that ``ex_intro`` should be declared as a hint.
 
 :tacn:`eauto` also obeys the following options:
 
-.. opt:: Info Eauto
-.. opt:: Debug Eauto
+.. flag:: Info Eauto
+          Debug Eauto
+          :undocumented:
 
 .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
@@ -3563,7 +3567,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
    .. note::
 
-      One can use an ``Extern`` hint with no pattern to do pattern-matching on
+      One can use an ``Extern`` hint with no pattern to do pattern matching on
       hypotheses using ``match goal`` with inside the tactic.
 
 
@@ -3859,7 +3863,7 @@ some incompatibilities.
    ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive
    types with one constructor and no indices, i.e. record-style connectives.
 
-.. opt:: Intuition Negation Unfolding
+.. flag:: Intuition Negation Unfolding
 
    Controls whether :tacn:`intuition` unfolds inner negations which do not need
    to be unfolded. This option is on by default.
@@ -3888,6 +3892,7 @@ usual logical connectives but instead may reason about any first-order class
 inductive definition.
 
 .. opt:: Firstorder Solver @tactic
+   :name: Firstorder Solver
 
    The default tactic used by :tacn:`firstorder` when no rule applies is
    :g:`auto with *`, it can be reset locally or globally using this option.
@@ -3916,6 +3921,7 @@ inductive definition.
   This combines the effects of the different variants of :tacn:`firstorder`.
 
 .. opt:: Firstorder Depth @num
+   :name: Firstorder Depth
 
    This option controls the proof-search depth bound.
 
@@ -3978,7 +3984,7 @@ match against it.
   additional arguments can be given to congruence by filling in the holes in the
   terms given in the error message, using the :tacn:`congruence with` variant described above.
 
-.. opt:: Congruence Verbose
+.. flag:: Congruence Verbose
 
   This option makes :tacn:`congruence` print debug information.