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, 18 insertions, 13 deletions

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.