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

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