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, 9 insertions, 9 deletions

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*