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

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 361b6e44a5..52609546d5 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -102,8 +102,8 @@ this corresponds to working in the following context:
    Unset Printing Implicit Defensive.
 
 .. seealso::
-   :opt:`Implicit Arguments`, :opt:`Strict Implicit`,
-   :opt:`Printing Implicit Defensive`
+   :flag:`Implicit Arguments`, :flag:`Strict Implicit`,
+   :flag:`Printing Implicit Defensive`
 
 .. _compatibility_issues_ssr:
 
@@ -2701,7 +2701,7 @@ typeclass inference.
   No inference for ``t``. Unresolved instances are
   quantified in the (inferred) type of ``t`` and abstracted in ``t``.
 
-.. opt:: SsrHave NoTCResolution
+.. flag:: SsrHave NoTCResolution
 
    This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses).
 
@@ -3865,7 +3865,7 @@ duplication of function arguments. These copies usually end up in
 types hidden by the implicit arguments machinery or by user-defined
 notations. In these situations computing the right occurrence numbers
 is very tedious because they must be counted on the goal as printed
-after setting the Printing All flag. Moreover the resulting script is
+after setting the :flag:`Printing All` flag. Moreover the resulting script is
 not really informative for the reader, since it refers to occurrence
 numbers he cannot easily see.