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:

2 files changed, 15 insertions, 21 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index ab1edc0b27..59cad3bea2 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -103,26 +103,23 @@ induction for objects in type `identᵢ`.
 Automatic declaration of schemes
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Elimination Schemes
+.. flag:: Elimination Schemes
 
-   It is possible to deactivate the automatic declaration of the
-   induction principles when defining a new inductive type with the
-   ``Unset Elimination Schemes`` command. It may be reactivated at any time with
-   ``Set Elimination Schemes``.
+   Enables automatic declaration of induction principles when defining a new
+   inductive type.  Defaults to on.
 
-.. opt:: Nonrecursive Elimination Schemes
+.. flag:: Nonrecursive Elimination Schemes
 
-   This option controls whether types declared with the keywords :cmd:`Variant` and
-   :cmd:`Record` get an automatic declaration of the induction principles.
+   Enables automatic declaration of induction principles for types declared with the :cmd:`Variant` and
+   :cmd:`Record` commands.  Defaults to off.
 
-.. opt:: Case Analysis Schemes
+.. flag:: Case Analysis Schemes
 
    This flag governs the generation of case analysis lemmas for inductive types,
-   i.e. corresponding to the pattern-matching term alone and without fixpoint.
+   i.e. corresponding to the pattern matching term alone and without fixpoint.
 
-.. opt:: Boolean Equality Schemes
-
-.. opt:: Decidable Equality Schemes
+.. flag:: Boolean Equality Schemes
+          Decidable Equality Schemes
 
    These flags control the automatic declaration of those Boolean equalities (see
    the second variant of ``Scheme``).
@@ -132,7 +129,7 @@ Automatic declaration of schemes
    You have to be careful with this option since Coq may now reject well-defined
    inductive types because it cannot compute a Boolean equality for them.
 
-.. opt:: Rewriting Schemes
+.. flag:: Rewriting Schemes
 
    This flag governs generation of equality-related schemes such as congruence.
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 0236f19490..705d67e6c6 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -376,17 +376,14 @@ for records. Here are examples:
 Displaying information about notations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Printing Notations
+.. flag:: Printing Notations
 
-   To deactivate the printing of all notations, use the command
-   ``Unset Printing Notations``. To reactivate it, use the command
-   ``Set Printing Notations``.
-
-   The default is to use notations for printing terms wherever possible.
+   Controls whether to use notations for printing terms wherever possible.
+   Default is on.
 
 .. seealso::
 
-   :opt:`Printing All`
+   :flag:`Printing All`
       To disable other elements in addition to notations.
 
 .. _locating-notations: