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:

8 files changed, 75 insertions, 73 deletions

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index ad6a06d2b0..cb267576b2 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -1,13 +1,13 @@
 .. _extendedpatternmatching:
 
-Extended pattern-matching
+Extended pattern matching
 =========================
 
 :Authors: Cristina Cornes and Hugo Herbelin
 
 .. TODO links to figures
 
-This section describes the full form of pattern-matching in |Coq| terms.
+This section describes the full form of pattern matching in |Coq| terms.
 
 .. |rhs| replace:: right hand sides
 
@@ -36,7 +36,7 @@ same values as ``pattern`` does and ``identifier`` is bound to the matched
 value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A
 list of patterns separated with commas is also considered as a pattern
 and is called *multiple pattern*. However multiple patterns can only
-occur at the root of pattern-matching equations. Disjunctions of
+occur at the root of pattern matching equations. Disjunctions of
 *multiple patterns* are allowed though.
 
 Since extended ``match`` expressions are compiled into the primitive ones,
@@ -44,7 +44,7 @@ the expressiveness of the theory remains the same. Once parsing has finished
 only simple patterns remain. The original nesting of the ``match`` expressions
 is recovered 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:`Printing Matching`), then by printing the term with :cmd:`Print`
+(use here :flag:`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*
@@ -86,7 +86,7 @@ Using multiple patterns in the definition of ``max`` lets us write:
 
 which will be compiled into the previous form.
 
-The pattern-matching compilation strategy examines patterns from left
+The pattern matching compilation strategy examines patterns from left
 to right. A match expression is generated **only** when there is at least
 one constructor in the column of patterns. E.g. the following example
 does not build a match expression.
@@ -260,9 +260,9 @@ When we use parameters in patterns there is an error message:
         | cons A _ l' => l'
         end).
 
-.. opt:: Asymmetric Patterns
+.. flag:: Asymmetric Patterns
 
-This option (off by default) removes parameters from constructors in patterns:
+   This flag (off by default) removes parameters from constructors in patterns:
 
 .. coqtop:: all
 
@@ -595,7 +595,7 @@ situation:
    incorrect (because constructors are not applied to the correct number of the
    arguments, because they are not linear or they are wrongly typed).
 
-.. exn:: Non exhaustive pattern-matching.
+.. exn:: Non exhaustive pattern matching.
 
    The pattern matching is not exhaustive.
 
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 4bfa45d54c..3d58f522dd 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -129,14 +129,14 @@ order to produce more readable code.
 
 The type-preserving optimizations are controlled by the following |Coq| options:
 
-.. opt:: Extraction Optimize
+.. flag:: 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
+.. flag:: 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
@@ -144,7 +144,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
+.. flag:: 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
@@ -153,7 +153,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
+.. flag:: Extraction AutoInline
 
    Default is on. The extraction mechanism inlines the bodies of
    some defined constants, according to some heuristics
@@ -225,7 +225,7 @@ When an actual extraction takes place, an error is normally raised if the
 if any of the implicit arguments still occurs in the final code.
 This behavior can be relaxed via the following option:
 
-.. opt:: Extraction SafeImplicits
+.. flag:: Extraction SafeImplicits
 
    Default is on. When this option is off, a warning is emitted
    instead of an error if some implicit arguments still occur in the
@@ -317,15 +317,15 @@ native boolean type instead of the |Coq| one. The syntax is the following:
    extractions for the type itself (first `string`) and all its
    constructors (all the `string` between square brackets). In this form,
    the ML extraction must be an ML inductive datatype, and the native
-   pattern-matching of the language will be used.
+   pattern matching of the language will be used.
 
 .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string
 
    Same as before, with a final extra `string` that indicates how to
-   perform pattern-matching over this inductive type. In this form,
+   perform pattern matching over this inductive type. In this form,
    the ML extraction could be an arbitrary type.
    For an inductive type with `k` constructors, the function used to
-   emulate the pattern-matching should expect `(k+1)` arguments, first the `k`
+   emulate the pattern matching should expect `(k+1)` arguments, first the `k`
    branches in functional form, and then the inductive element to
    destruct. For instance, the match branch ``| S n => foo`` gives the
    functional form ``(fun n -> foo)``. Note that a constructor with no
@@ -342,7 +342,7 @@ native boolean type instead of the |Coq| one. The syntax is the following:
 
   * Extracting an inductive type to a pre-existing ML inductive type
     is quite sound. But extracting to a general type (by providing an
-    ad-hoc pattern-matching) will often **not** be fully rigorously
+    ad-hoc pattern matching) will often **not** be fully rigorously
     correct. For instance, when extracting ``nat`` to |OCaml| ``int``,
     it is theoretically possible to build ``nat`` values that are
     larger than |OCaml| ``max_int``. It is the user's responsibility to
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 5cb0eaf469..fc5a366caf 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -254,19 +254,16 @@ Displaying Available Coercions
 Activating the Printing of Coercions
 -------------------------------------
 
-.. opt:: Printing Coercions
+.. flag:: Printing Coercions
 
    When on, this option forces all the coercions to be printed.
    By default, coercions are not printed.
 
-.. cmd:: Add Printing Coercion @qualid
+.. table:: Printing Coercion @qualid
+   :name: Printing Coercion
 
-   This command forces coercion denoted by :n:`@qualid` to be printed.
-   By default, a coercion is never printed.
-
-.. cmd:: Remove Printing Coercion @qualid
-
-   Use this command, to skip the printing of coercion :n:`@qualid`.
+   Specifies a set of qualids for which coercions are always displayed.  Use the
+   :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids.
 
 .. _coercions-classes-as-records:
 
@@ -313,7 +310,7 @@ are also forgotten.
 Coercions and Modules
 ---------------------
 
-.. opt:: Automatic Coercions Import
+.. flag:: 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
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index f7a431ef29..828505b850 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -116,23 +116,23 @@ loaded by
 Options
 -------
 
-.. opt:: Stable Omega
+.. flag:: Stable Omega
 
    .. deprecated:: 8.5
 
    This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
    resets internal name counters to make executions of :tacn:`omega` independent.
 
-.. opt:: Omega UseLocalDefs
+.. flag:: Omega UseLocalDefs
 
    This option (on by default) allows :tacn:`omega` to use the bodies of local
    variables.
 
-.. opt:: Omega System
+.. flag:: Omega System
 
    This option (off by default) activate the printing of debug information
 
-.. opt:: Omega Action
+.. flag:: Omega Action
 
    This option (off by default) activate the printing of debug information
 
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index eb19d57203..8b7214e2ab 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -58,7 +58,7 @@ variables used.
 Automatic suggestion of proof annotations
 `````````````````````````````````````````
 
-The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed``
+The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed``
 command is processed, a correct proof annotation. It is up to the user
 to modify the proof script accordingly.
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 24247f7bb1..fad45995d2 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -42,7 +42,7 @@ be considered as an object of type :g:`{x : T | P}` for any well-formed
 will generate an obligation for every such coercion. In the other direction,
 Russell will automatically insert a projection.
 
-Another distinction is the treatment of pattern-matching. Apart from
+Another distinction is the treatment of pattern matching. Apart from
 the following differences, it is equivalent to the standard match
 operation (see :ref:`extendedpatternmatching`).
 
@@ -81,15 +81,15 @@ operation (see :ref:`extendedpatternmatching`).
 There are options to control the generation of equalities and
 coercions.
 
-.. opt:: Program Cases
+.. flag:: Program Cases
 
-   This controls the special treatment of pattern-matching generating equalities
+   This controls the special treatment of pattern matching generating equalities
    and disequalities when using |Program| (it is on by default). All
    pattern-matches and let-patterns are handled using the standard algorithm
    of |Coq| (see :ref:`extendedpatternmatching`) when this option is
    deactivated.
 
-.. opt:: Program Generalized Coercion
+.. flag:: Program Generalized Coercion
 
    This controls the coercion of general inductive types when using |Program|
    (the option is on by default). Coercion of subset types and pairs is still
@@ -102,7 +102,7 @@ Syntactic control over equalities
 
 To give more control over the generation of equalities, the
 type checker will fall back directly to |Coq|’s usual typing of dependent
-pattern-matching if a return or in clause is specified. Likewise, the
+pattern matching if a return or in clause is specified. Likewise, the
 if construct is not treated specially by |Program| so boolean tests in
 the code are not automatically reflected in the obligations. One can
 use the :g:`dec` combinator to get the correct hypotheses as in:
@@ -210,7 +210,7 @@ with mutually recursive definitions too.
      end.
 
 Here we have one obligation for each branch (branches for :g:`0` and
-``(S 0)`` are automatically generated by the pattern-matching
+``(S 0)`` are automatically generated by the pattern matching
 compilation algorithm).
 
 .. coqtop:: all
@@ -317,19 +317,19 @@ optional tactic is replaced by the default one if not specified.
    Shows the term that will be fed to the kernel once the obligations
    are solved. Useful for debugging.
 
-.. opt:: Transparent Obligations
+.. flag:: Transparent Obligations
 
    Controls whether all obligations should be declared as transparent
    (the default), or if the system should infer which obligations can be
    declared opaque.
 
-.. opt:: Hide Obligations
+.. flag:: Hide Obligations
 
    Controls whether obligations appearing in the
    term should be hidden as implicit arguments of the special
    constantProgram.Tactics.obligation.
 
-.. opt:: Shrink Obligations
+.. flag:: Shrink Obligations
 
    *Deprecated since 8.7*
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 418014809f..369dae0ead 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -456,7 +456,7 @@ This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``.
 Options
 ~~~~~~~
 
-.. opt:: Typeclasses Dependency Order
+.. flag:: Typeclasses Dependency Order
 
    This option (on by default since 8.6) respects the dependency order
    between subgoals, meaning that subgoals on which other subgoals depend
@@ -465,7 +465,7 @@ Options
    quite different performance behaviors of proof search.
 
 
-.. opt:: Typeclasses Filtered Unification
+.. flag:: 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
@@ -479,7 +479,7 @@ Options
    where there is a hole in that place.
 
 
-.. opt:: Typeclasses Limit Intros
+.. flag:: 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
@@ -493,7 +493,7 @@ Options
       status of the product introduction rule, resulting in potentially more
       expensive proof-search (i.e. more useless backtracking).
 
-.. opt:: Typeclass Resolution For Conversion
+.. flag:: 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
@@ -501,7 +501,7 @@ Options
    resolution is tried before launching unification once again.
 
 
-.. opt:: Typeclasses Strict Resolution
+.. flag:: Typeclasses Strict Resolution
 
    Typeclass declarations introduced when this option is set have a
    stricter resolution behavior (the option is off by default). When
@@ -511,28 +511,33 @@ Options
    instantiated.
 
 
-.. opt:: Typeclasses Unique Solutions
+.. flag:: 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.
 
 
-.. opt:: Typeclasses Unique Instances
+.. flag:: 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.
 
-.. opt:: Typeclasses Debug {? Verbosity @num}
+.. flag:: Typeclasses Debug
 
-   These options allow to see the resolution steps of typeclasses that are
-   performed during search. The ``Debug`` option is synonymous to ``Debug
-   Verbosity 1``, and ``Debug Verbosity 2`` provides more information
-   (tried tactics, shelving of goals, etc…).
+   Controls whether typeclass resolution steps are shown during search.  Setting this flag
+   also sets :opt:`Typeclasses Debug Verbosity` to 1.
 
-.. opt:: Refine Instance Mode
+.. opt:: Typeclasses Debug Verbosity @num
+   :name: Typeclasses Debug Verbosity
+
+   Determines how much information is shown for typeclass resolution steps during search.
+   1 is the default level.  2 shows additional information such as tried tactics and shelving
+   of goals.  Setting this option also sets :flag:`Typeclasses Debug`.
+
+.. flag:: Refine Instance Mode
 
    This option allows to switch the behavior of instance declarations made through
    the Instance command.
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 706ce1065c..41afe3c312 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -57,7 +57,7 @@ so:
    Definition selfpid := pidentity (@pidentity).
 
 Of course, the two instances of :g:`pidentity` in this definition are
-different. This can be seen when the :opt:`Printing Universes` option is on:
+different. This can be seen when the :flag:`Printing Universes` flag is on:
 
 .. coqtop:: none
 
@@ -77,7 +77,7 @@ levels.
 
 When printing :g:`pidentity`, we can see the universes it binds in
 the annotation :g:`@{Top.2}`. Additionally, when
-:opt:`Printing Universes` is on we print the "universe context" of
+:flag:`Printing Universes` is on we print the "universe context" of
 :g:`pidentity` consisting of the bound universes and the
 constraints they must verify (for :g:`pidentity` there are no constraints).
 
@@ -127,14 +127,14 @@ Polymorphic, Monomorphic
    As shown in the examples, polymorphic definitions and inductives can be
    declared using the ``Polymorphic`` prefix.
 
-.. opt:: Universe Polymorphism
+.. flag:: Universe Polymorphism
 
    Once enabled, this option will implicitly prepend ``Polymorphic`` to any
    definition of the user.
 
 .. cmd:: Monomorphic @definition
 
-   When the :opt:`Universe Polymorphism` option is set, to make a definition
+   When the :flag:`Universe Polymorphism` option is set, to make a definition
    producing global universe constraints, one can use the ``Monomorphic`` prefix.
 
 Many other commands support the ``Polymorphic`` flag, including:
@@ -167,7 +167,7 @@ declared cumulative using the :g:`Cumulative` prefix.
 
    Declares the inductive as cumulative
 
-Alternatively, there is an option :opt:`Polymorphic Inductive
+Alternatively, there is a flag :flag:`Polymorphic Inductive
 Cumulativity` which when set, makes all subsequent *polymorphic*
 inductive definitions cumulative.  When set, inductive types and the
 like can be enforced to be non-cumulative using the :g:`NonCumulative`
@@ -177,7 +177,7 @@ prefix.
 
    Declares the inductive as non-cumulative
 
-.. opt:: Polymorphic Inductive Cumulativity
+.. flag:: Polymorphic Inductive Cumulativity
 
    When this option is on, it sets all following polymorphic inductive
    types as cumulative (it is off by default).
@@ -227,7 +227,7 @@ Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
 error is issued whenever the user uses the :g:`Cumulative` or
 :g:`NonCumulative` prefix in a monomorphic context.
-Notice that this is not the case for the option :opt:`Polymorphic Inductive Cumulativity`.
+Notice that this is not the case for the option :flag:`Polymorphic Inductive Cumulativity`.
 That is, this option, when set, makes all subsequent *polymorphic*
 inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used)
 but has no effect on *monomorphic* inductive declarations.
@@ -275,18 +275,18 @@ An example of a proof using cumulativity
 Cumulativity Weak Constraints
 -----------------------------
 
-.. opt:: Cumulativity Weak Constraints
+.. flag:: Cumulativity Weak Constraints
 
-This option, on by default, causes "weak" constraints to be produced
-when comparing universes in an irrelevant position. Processing weak
-constraints is delayed until minimization time. A weak constraint
-between `u` and `v` when neither is smaller than the other and
-one is flexible causes them to be unified. Otherwise the constraint is
-silently discarded.
+   When set, which is the default, causes "weak" constraints to be produced
+   when comparing universes in an irrelevant position. Processing weak
+   constraints is delayed until minimization time. A weak constraint
+   between `u` and `v` when neither is smaller than the other and
+   one is flexible causes them to be unified. Otherwise the constraint is
+   silently discarded.
 
-This heuristic is experimental and may change in future versions.
-Disabling weak constraints is more predictable but may produce
-arbitrary numbers of universes.
+   This heuristic is experimental and may change in future versions.
+   Disabling weak constraints is more predictable but may produce
+   arbitrary numbers of universes.
 
 
 Global and local universes
@@ -352,9 +352,9 @@ This minimization process is applied only to fresh universe variables.
 It simply adds an equation between the variable and its lower bound if
 it is an atomic universe (i.e. not an algebraic max() universe).
 
-.. opt:: Universe Minimization ToSet
+.. flag:: Universe Minimization ToSet
 
-   Turning this option off (it is on by default) disallows minimization
+   Turning this flag off (it is on by default) disallows minimization
    to the sort :g:`Set` and only collapses floating universes between
    themselves.
 
@@ -434,7 +434,7 @@ underscore or by omitting the annotation to a polymorphic definition.
    Check le@{k _}.
    Check le.
 
-.. opt:: Strict Universe Declaration.
+.. flag:: Strict Universe Declaration
 
    Turning this option off allows one to freely use
    identifiers for universes without declaring them first, with the