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:
author: Jim Fehrle 2018-09-01 12:39:09 -0700
committer: Jim Fehrle 2018-09-20 18:27:08 -0700
commit: ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 (patch)
tree: 2f73dd477ac9276ba8ed9409aab613370d29c7fb /doc
parent: d4b5de427d94d82f09d58e0f1095f052a5900914 (diff)
20 files changed, 414 insertions, 472 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index ad6a06d2b0..cb267576b2 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -1,13 +1,13 @@
 .. _extendedpatternmatching:
 
-Extended pattern-matching
+Extended pattern matching
 =========================
 
 :Authors: Cristina Cornes and Hugo Herbelin
 
 .. TODO links to figures
 
-This section describes the full form of pattern-matching in |Coq| terms.
+This section describes the full form of pattern matching in |Coq| terms.
 
 .. |rhs| replace:: right hand sides
 
@@ -36,7 +36,7 @@ same values as ``pattern`` does and ``identifier`` is bound to the matched
 value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A
 list of patterns separated with commas is also considered as a pattern
 and is called *multiple pattern*. However multiple patterns can only
-occur at the root of pattern-matching equations. Disjunctions of
+occur at the root of pattern matching equations. Disjunctions of
 *multiple patterns* are allowed though.
 
 Since extended ``match`` expressions are compiled into the primitive ones,
@@ -44,7 +44,7 @@ the expressiveness of the theory remains the same. Once parsing has finished
 only simple patterns remain. The original nesting of the ``match`` expressions
 is recovered at printing time. An easy way to see the result
 of the expansion is to toggle off the nesting performed at printing
-(use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print`
+(use here :flag:`Printing Matching`), then by printing the term with :cmd:`Print`
 if the term is a constant, or using the command :cmd:`Check`.
 
 The extended ``match`` still accepts an optional *elimination predicate*
@@ -86,7 +86,7 @@ Using multiple patterns in the definition of ``max`` lets us write:
 
 which will be compiled into the previous form.
 
-The pattern-matching compilation strategy examines patterns from left
+The pattern matching compilation strategy examines patterns from left
 to right. A match expression is generated **only** when there is at least
 one constructor in the column of patterns. E.g. the following example
 does not build a match expression.
@@ -260,9 +260,9 @@ When we use parameters in patterns there is an error message:
         | cons A _ l' => l'
         end).
 
-.. opt:: Asymmetric Patterns
+.. flag:: Asymmetric Patterns
 
-This option (off by default) removes parameters from constructors in patterns:
+   This flag (off by default) removes parameters from constructors in patterns:
 
 .. coqtop:: all
 
@@ -595,7 +595,7 @@ situation:
    incorrect (because constructors are not applied to the correct number of the
    arguments, because they are not linear or they are wrongly typed).
 
-.. exn:: Non exhaustive pattern-matching.
+.. exn:: Non exhaustive pattern matching.
 
    The pattern matching is not exhaustive.
 
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 4bfa45d54c..3d58f522dd 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -129,14 +129,14 @@ order to produce more readable code.
 
 The type-preserving optimizations are controlled by the following |Coq| options:
 
-.. opt:: Extraction Optimize
+.. flag:: Extraction Optimize
 
    Default is on. This controls all type-preserving optimizations made on
    the ML terms (mostly reduction of dummy beta/iota redexes, but also
    simplifications on Cases, etc). Turn this option off if you want a
    ML term as close as possible to the Coq term.
 
-.. opt:: Extraction Conservative Types
+.. flag:: Extraction Conservative Types
 
    Default is off. This controls the non type-preserving optimizations
    made on ML terms (which try to avoid function abstraction of dummy
@@ -144,7 +144,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted
    code of ``e`` and ``t`` respectively.
 
-.. opt:: Extraction KeepSingleton
+.. flag:: Extraction KeepSingleton
 
    Default is off. Normally, when the extraction of an inductive type
    produces a singleton type (i.e. a type with only one constructor, and
@@ -153,7 +153,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    The typical example is ``sig``. This option allows disabling this
    optimization when one wishes to preserve the inductive structure of types.
 
-.. opt:: Extraction AutoInline
+.. flag:: Extraction AutoInline
 
    Default is on. The extraction mechanism inlines the bodies of
    some defined constants, according to some heuristics
@@ -225,7 +225,7 @@ When an actual extraction takes place, an error is normally raised if the
 if any of the implicit arguments still occurs in the final code.
 This behavior can be relaxed via the following option:
 
-.. opt:: Extraction SafeImplicits
+.. flag:: Extraction SafeImplicits
 
    Default is on. When this option is off, a warning is emitted
    instead of an error if some implicit arguments still occur in the
@@ -317,15 +317,15 @@ native boolean type instead of the |Coq| one. The syntax is the following:
    extractions for the type itself (first `string`) and all its
    constructors (all the `string` between square brackets). In this form,
    the ML extraction must be an ML inductive datatype, and the native
-   pattern-matching of the language will be used.
+   pattern matching of the language will be used.
 
 .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string
 
    Same as before, with a final extra `string` that indicates how to
-   perform pattern-matching over this inductive type. In this form,
+   perform pattern matching over this inductive type. In this form,
    the ML extraction could be an arbitrary type.
    For an inductive type with `k` constructors, the function used to
-   emulate the pattern-matching should expect `(k+1)` arguments, first the `k`
+   emulate the pattern matching should expect `(k+1)` arguments, first the `k`
    branches in functional form, and then the inductive element to
    destruct. For instance, the match branch ``| S n => foo`` gives the
    functional form ``(fun n -> foo)``. Note that a constructor with no
@@ -342,7 +342,7 @@ native boolean type instead of the |Coq| one. The syntax is the following:
 
   * Extracting an inductive type to a pre-existing ML inductive type
     is quite sound. But extracting to a general type (by providing an
-    ad-hoc pattern-matching) will often **not** be fully rigorously
+    ad-hoc pattern matching) will often **not** be fully rigorously
     correct. For instance, when extracting ``nat`` to |OCaml| ``int``,
     it is theoretically possible to build ``nat`` values that are
     larger than |OCaml| ``max_int``. It is the user's responsibility to
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
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index f7a431ef29..828505b850 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -116,23 +116,23 @@ loaded by
 Options
 -------
 
-.. opt:: Stable Omega
+.. flag:: Stable Omega
 
    .. deprecated:: 8.5
 
    This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
    resets internal name counters to make executions of :tacn:`omega` independent.
 
-.. opt:: Omega UseLocalDefs
+.. flag:: Omega UseLocalDefs
 
    This option (on by default) allows :tacn:`omega` to use the bodies of local
    variables.
 
-.. opt:: Omega System
+.. flag:: Omega System
 
    This option (off by default) activate the printing of debug information
 
-.. opt:: Omega Action
+.. flag:: Omega Action
 
    This option (off by default) activate the printing of debug information
 
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index eb19d57203..8b7214e2ab 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -58,7 +58,7 @@ variables used.
 Automatic suggestion of proof annotations
 `````````````````````````````````````````
 
-The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed``
+The flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed``
 command is processed, a correct proof annotation. It is up to the user
 to modify the proof script accordingly.
 
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*
 
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.
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 706ce1065c..41afe3c312 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -57,7 +57,7 @@ so:
    Definition selfpid := pidentity (@pidentity).
 
 Of course, the two instances of :g:`pidentity` in this definition are
-different. This can be seen when the :opt:`Printing Universes` option is on:
+different. This can be seen when the :flag:`Printing Universes` flag is on:
 
 .. coqtop:: none
 
@@ -77,7 +77,7 @@ levels.
 
 When printing :g:`pidentity`, we can see the universes it binds in
 the annotation :g:`@{Top.2}`. Additionally, when
-:opt:`Printing Universes` is on we print the "universe context" of
+:flag:`Printing Universes` is on we print the "universe context" of
 :g:`pidentity` consisting of the bound universes and the
 constraints they must verify (for :g:`pidentity` there are no constraints).
 
@@ -127,14 +127,14 @@ Polymorphic, Monomorphic
    As shown in the examples, polymorphic definitions and inductives can be
    declared using the ``Polymorphic`` prefix.
 
-.. opt:: Universe Polymorphism
+.. flag:: Universe Polymorphism
 
    Once enabled, this option will implicitly prepend ``Polymorphic`` to any
    definition of the user.
 
 .. cmd:: Monomorphic @definition
 
-   When the :opt:`Universe Polymorphism` option is set, to make a definition
+   When the :flag:`Universe Polymorphism` option is set, to make a definition
    producing global universe constraints, one can use the ``Monomorphic`` prefix.
 
 Many other commands support the ``Polymorphic`` flag, including:
@@ -167,7 +167,7 @@ declared cumulative using the :g:`Cumulative` prefix.
 
    Declares the inductive as cumulative
 
-Alternatively, there is an option :opt:`Polymorphic Inductive
+Alternatively, there is a flag :flag:`Polymorphic Inductive
 Cumulativity` which when set, makes all subsequent *polymorphic*
 inductive definitions cumulative.  When set, inductive types and the
 like can be enforced to be non-cumulative using the :g:`NonCumulative`
@@ -177,7 +177,7 @@ prefix.
 
    Declares the inductive as non-cumulative
 
-.. opt:: Polymorphic Inductive Cumulativity
+.. flag:: Polymorphic Inductive Cumulativity
 
    When this option is on, it sets all following polymorphic inductive
    types as cumulative (it is off by default).
@@ -227,7 +227,7 @@ Cumulative inductive types, coninductive types, variants and records
 only make sense when they are universe polymorphic. Therefore, an
 error is issued whenever the user uses the :g:`Cumulative` or
 :g:`NonCumulative` prefix in a monomorphic context.
-Notice that this is not the case for the option :opt:`Polymorphic Inductive Cumulativity`.
+Notice that this is not the case for the option :flag:`Polymorphic Inductive Cumulativity`.
 That is, this option, when set, makes all subsequent *polymorphic*
 inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used)
 but has no effect on *monomorphic* inductive declarations.
@@ -275,18 +275,18 @@ An example of a proof using cumulativity
 Cumulativity Weak Constraints
 -----------------------------
 
-.. opt:: Cumulativity Weak Constraints
+.. flag:: Cumulativity Weak Constraints
 
-This option, on by default, causes "weak" constraints to be produced
-when comparing universes in an irrelevant position. Processing weak
-constraints is delayed until minimization time. A weak constraint
-between `u` and `v` when neither is smaller than the other and
-one is flexible causes them to be unified. Otherwise the constraint is
-silently discarded.
+   When set, which is the default, causes "weak" constraints to be produced
+   when comparing universes in an irrelevant position. Processing weak
+   constraints is delayed until minimization time. A weak constraint
+   between `u` and `v` when neither is smaller than the other and
+   one is flexible causes them to be unified. Otherwise the constraint is
+   silently discarded.
 
-This heuristic is experimental and may change in future versions.
-Disabling weak constraints is more predictable but may produce
-arbitrary numbers of universes.
+   This heuristic is experimental and may change in future versions.
+   Disabling weak constraints is more predictable but may produce
+   arbitrary numbers of universes.
 
 
 Global and local universes
@@ -352,9 +352,9 @@ This minimization process is applied only to fresh universe variables.
 It simply adds an equation between the variable and its lower bound if
 it is an atomic universe (i.e. not an algebraic max() universe).
 
-.. opt:: Universe Minimization ToSet
+.. flag:: Universe Minimization ToSet
 
-   Turning this option off (it is on by default) disallows minimization
+   Turning this flag off (it is on by default) disallows minimization
    to the sort :g:`Set` and only collapses floating universes between
    themselves.
 
@@ -434,7 +434,7 @@ underscore or by omitting the annotation to a polymorphic definition.
    Check le@{k _}.
    Check le.
 
-.. opt:: Strict Universe Declaration.
+.. flag:: Strict Universe Declaration
 
    Turning this option off allows one to freely use
    identifiers for universes without declaring them first, with the
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index be6fe5704e..212f0a65b0 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -196,7 +196,7 @@ between sorts.
 The new version provides powerful tools for easier developments.
 
 Cristina Cornes designed an extension of the |Coq| syntax to allow
-definition of terms using a powerful pattern-matching analysis in the
+definition of terms using a powerful pattern matching analysis in the
 style of ML programs.
 
 Amokrane Saïbi wrote a mechanism to simulate inheritance between types
@@ -240,7 +240,7 @@ names to Caml functions corresponding to |Coq| tactic names.
 Bruno Barras wrote new, more efficient reduction functions.
 
 Hugo Herbelin introduced more uniform notations in the |Coq| specification
-language: the definitions by fixpoints and pattern-matching have a more
+language: the definitions by fixpoints and pattern matching have a more
 readable syntax. Patrick Loiseleur introduced user-friendly notations
 for arithmetic expressions.
 
@@ -317,14 +317,14 @@ modules and also to get closer to a certified kernel.
 
 Hugo Herbelin introduced a new structure of terms with local
 definitions. He introduced “qualified” names, wrote a new
-pattern-matching compilation algorithm and designed a more compact
+pattern matching compilation algorithm and designed a more compact
 algorithm for checking the logical consistency of universes. He
 contributed to the simplification of |Coq| internal structures and the
 optimisation of the system. He added basic tactics for forward reasoning
 and coercions in patterns.
 
 David Delahaye introduced a new language for tactics. General tactics
-using pattern-matching on goals and context can directly be written from
+using pattern matching on goals and context can directly be written from
 the |Coq| toplevel. He also provided primitives for the design of
 user-defined tactics in Caml.
 
@@ -615,8 +615,8 @@ with the library of integers he developed.
 
 Beside the libraries, various improvements were contributed to provide a more
 comfortable end-user language and more expressive tactic language. Hugo
-Herbelin and Matthieu Sozeau improved the pattern-matching compilation
-algorithm (detection of impossible clauses in pattern-matching,
+Herbelin and Matthieu Sozeau improved the pattern matching compilation
+algorithm (detection of impossible clauses in pattern matching,
 automatic inference of the return type). Hugo Herbelin, Pierre Letouzey
 and Matthieu Sozeau contributed various new convenient syntactic
 constructs and new tactics or tactic features: more inference of
@@ -792,7 +792,7 @@ through :math:`\beta`-redexes that are blocked by the “match”
 construction (blocked commutative cuts).
 
 Relying on the added permissiveness of the guard condition, Hugo
-Herbelin could extend the pattern-matching compilation algorithm so that
+Herbelin could extend the pattern matching compilation algorithm so that
 matching over a sequence of terms involving dependencies of a term or of
 the indices of the type of a term in the type of other terms is
 systematically supported.
@@ -970,7 +970,7 @@ principle than the previously added :math:`\eta`-conversion for function
 types, based on formulations of the Calculus of Inductive Constructions
 with typed equality. Primitive projections, which do not carry the
 parameters of the record and are rigid names (not defined as a
-pattern-matching construct), make working with nested records more
+pattern matching construct), make working with nested records more
 manageable in terms of time and space consumption. This extension and
 universe polymorphism were carried out partly while Matthieu Sozeau was
 working at the IAS in Princeton.
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index c8c3e37efb..381f8bb661 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1025,21 +1025,21 @@ Template polymorphism
 Inductive types can be made polymorphic over their arguments
 in :math:`\Type`.
 
-.. opt:: Auto Template Polymorphism
+.. flag:: Auto Template Polymorphism
 
-  This option, enabled by default, makes every inductive type declared
-  at level :math:`Type` (without annotations or hiding it behind a
-  definition) template polymorphic.
+   This option, enabled by default, makes every inductive type declared
+   at level :math:`Type` (without annotations or hiding it behind a
+   definition) template polymorphic.
 
-  This can be prevented using the ``notemplate`` attribute.
+   This can be prevented using the ``notemplate`` attribute.
 
-  An inductive type can be forced to be template polymorphic using the
-  ``template`` attribute.
+   An inductive type can be forced to be template polymorphic using the
+   ``template`` attribute.
 
-  Template polymorphism and universe polymorphism (see Chapter
-  :ref:`polymorphicuniverses`) are incompatible, so if the later is
-  enabled it will prevail over automatic template polymorphism and
-  cause an error when using the ``template`` attribute.
+   Template polymorphism and universe polymorphism (see Chapter
+   :ref:`polymorphicuniverses`) are incompatible, so if the later is
+   enabled it will prevail over automatic template polymorphism and
+   cause an error when using the ``template`` attribute.
 
 If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
 for the arity obtained from :math:`A` by replacing its sort with :math:`s`.
@@ -1120,7 +1120,7 @@ and otherwise in the Type hierarchy.
 
 Note that the side-condition about allowed elimination sorts in the
 rule **Ind-Family** is just to avoid to recompute the allowed elimination
-sorts at each instance of a pattern-matching (see Section :ref:`Destructors`). As
+sorts at each instance of a pattern matching (see Section :ref:`Destructors`). As
 an example, let us consider the following definition:
 
 .. example::
@@ -1244,7 +1244,7 @@ primitive recursion over the structure.
 But this operator is rather tedious to implement and use. We choose in
 this version of |Coq| to factorize the operator for primitive recursion
 into two more primitive operations as was first suggested by Th.
-Coquand in :cite:`Coq92`. One is the definition by pattern-matching. The
+Coquand in :cite:`Coq92`. One is the definition by pattern matching. The
 second one is a definition by guarded fixpoints.
 
 
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 320448d46e..85474a3e98 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -618,7 +618,7 @@ Finally, it gives the definition of the usual orderings ``le``,
 
 Properties of these relations are not initially known, but may be
 required by the user from modules ``Le`` and ``Lt``.  Finally,
-``Peano`` gives some lemmas allowing pattern-matching, and a double
+``Peano`` gives some lemmas allowing pattern matching, and a double
 induction principle.
 
 .. index::
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 27ed176a9b..636144e0c8 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -100,19 +100,25 @@ to be all present if the missing ones can be inferred or prompted for
        Rat_bottom_cond := O_S 1;
        Rat_irred_cond := one_two_irred |}.
 
-This syntax can be disabled globally for printing by
+The following settings let you control the display format for types:
 
-.. cmd:: Unset Printing Records
+.. flag:: Printing Records
 
-For a given type, one can override this using either
+   If set, use the record syntax (shown above) as the default display format.
 
-.. cmd:: Add Printing Record @ident
+You can override the display format for specified types by adding entries to these tables:
 
-to get record syntax or
+.. table:: Printing Record @qualid
+   :name: Printing Record
 
-.. cmd:: Add Printing Constructor @ident
+   Specifies a set of qualids which are displayed as records.  Use the
+   :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids.
 
-to get constructor syntax.
+.. table:: Printing Constructor @qualid
+   :name: Printing Constructor
+
+   Specifies a set of qualids which are displayed as constructors.  Use the
+   :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids.
 
 This syntax can also be used for pattern matching.
 
@@ -145,7 +151,7 @@ available:
 
 It can be activated for printing with
 
-.. opt:: Printing Projections
+.. flag:: Printing Projections
 
 .. example::
 
@@ -221,35 +227,35 @@ the errors of inductive definitions, as described in Section
 Primitive Projections
 ~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Primitive Projections
+.. flag:: Primitive Projections
 
-Turns on the use of primitive
-projections when defining subsequent records (even through the ``Inductive``
-and ``CoInductive`` commands). Primitive projections
-extended the Calculus of Inductive Constructions with a new binary
-term constructor `r.(p)` representing a primitive projection `p` applied
-to a record object `r` (i.e., primitive projections are always applied).
-Even if the record type has parameters, these do not appear at
-applications of the projection, considerably reducing the sizes of
-terms when manipulating parameterized records and type checking time.
-On the user level, primitive projections can be used as a replacement
-for the usual defined ones, although there are a few notable differences.
+   Turns on the use of primitive
+   projections when defining subsequent records (even through the ``Inductive``
+   and ``CoInductive`` commands). Primitive projections
+   extended the Calculus of Inductive Constructions with a new binary
+   term constructor `r.(p)` representing a primitive projection `p` applied
+   to a record object `r` (i.e., primitive projections are always applied).
+   Even if the record type has parameters, these do not appear at
+   applications of the projection, considerably reducing the sizes of
+   terms when manipulating parameterized records and type checking time.
+   On the user level, primitive projections can be used as a replacement
+   for the usual defined ones, although there are a few notable differences.
 
-.. opt:: Printing Primitive Projection Parameters
+.. flag:: Printing Primitive Projection Parameters
 
-This compatibility option reconstructs internally omitted parameters at
-printing time (even though they are absent in the actual AST manipulated
-by the kernel).
+   This compatibility option reconstructs internally omitted parameters at
+   printing time (even though they are absent in the actual AST manipulated
+   by the kernel).
 
-.. opt:: Printing Primitive Projection Compatibility
+.. flag:: Printing Primitive Projection Compatibility
 
-This compatibility option (on by default) governs the
-printing of pattern-matching over primitive records.
+   This compatibility option (on by default) governs the
+   printing of pattern matching over primitive records.
 
 Primitive Record Types
 ++++++++++++++++++++++
 
-When the :opt:`Primitive Projections` option is on, definitions of
+When the :flag:`Primitive Projections` option is on, definitions of
 record types change meaning. When a type is declared with primitive
 projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though).
 To eliminate the (co-)inductive type, one must use its defined primitive projections.
@@ -259,9 +265,9 @@ To eliminate the (co-)inductive type, one must use its defined primitive project
 For compatibility, the parameters still appear to the user when
 printing terms even though they are absent in the actual AST
 manipulated by the kernel. This can be changed by unsetting the
-``Printing Primitive Projection Parameters`` flag. Further compatibility
+:flag:`Printing Primitive Projection Parameters` flag. Further compatibility
 printing can be deactivated thanks to the ``Printing Primitive Projection
-Compatibility`` option which governs the printing of pattern-matching
+Compatibility`` option which governs the printing of pattern matching
 over primitive records.
 
 There are currently two ways to introduce primitive records types:
@@ -291,7 +297,7 @@ the folded version delta-reduces to the unfolded version. This allows to
 precisely mimic the usual unfolding rules of constants. Projections
 obey the usual ``simpl`` flags of the ``Arguments`` command in particular.
 There is currently no way to input unfolded primitive projections at the
-user-level, and one must use the ``Printing Primitive Projection Compatibility``
+user-level, and one must use the :flag:`Printing Primitive Projection Compatibility`
 to display unfolded primitive projections as matches and distinguish them from folded ones.
 
 
@@ -304,7 +310,7 @@ an object of the record type as arguments, and whose body is an
 application of the unfolded primitive projection of the same name. These
 constants are used when elaborating partial applications of the
 projection. One can distinguish them from applications of the primitive
-projection if the ``Printing Primitive Projection Parameters`` option
+projection if the :flag`Printing Primitive Projection Parameters` option
 is off: For a primitive projection application, parameters are printed
 as underscores while for the compatibility projections they are printed
 as usual.
@@ -318,17 +324,17 @@ Variants and extensions of :g:`match`
 
 .. _mult-match:
 
-Multiple and nested pattern-matching
+Multiple and nested pattern matching
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The basic version of :g:`match` allows pattern-matching on simple
+The basic version of :g:`match` allows pattern matching on simple
 patterns. As an extension, multiple nested patterns or disjunction of
 patterns are allowed, as in ML-like languages.
 
 The extension just acts as a macro that is expanded during parsing
 into a sequence of match on simple patterns. Especially, a
 construction defined using the extended match is generally printed
-under its expanded form (see :opt:`Printing Matching`).
+under its expanded form (see :flag:`Printing Matching`).
 
 .. seealso:: :ref:`extendedpatternmatching`.
 
@@ -337,7 +343,7 @@ under its expanded form (see :opt:`Printing Matching`).
 Pattern-matching on boolean values: the if expression
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-For inductive types with exactly two constructors and for pattern-matching
+For inductive types with exactly two constructors and for pattern matching
 expressions that do not depend on the arguments of the constructors, it is possible
 to use a ``if … then … else`` notation. For instance, the definition
 
@@ -476,123 +482,93 @@ of :g:`match` expressions.
 Printing nested patterns
 +++++++++++++++++++++++++
 
-.. opt:: Printing Matching
+.. flag:: Printing Matching
 
-The Calculus of Inductive Constructions knows pattern-matching only
-over simple patterns. It is however convenient to re-factorize nested
-pattern-matching into a single pattern-matching over a nested
-pattern.
+   The Calculus of Inductive Constructions knows pattern matching only
+   over simple patterns. It is however convenient to re-factorize nested
+   pattern matching into a single pattern matching over a nested
+   pattern.
 
-When this option is on (default), |Coq|’s printer tries to do such
-limited re-factorization.
-Turning it off tells |Coq| to print only simple pattern-matching problems
-in the same way as the |Coq| kernel handles them.
+   When this option is on (default), |Coq|’s printer tries to do such
+   limited re-factorization.
+   Turning it off tells |Coq| to print only simple pattern matching problems
+   in the same way as the |Coq| kernel handles them.
 
 
 Factorization of clauses with same right-hand side
 ++++++++++++++++++++++++++++++++++++++++++++++++++
 
-.. opt:: Printing Factorizable Match Patterns
+.. flag:: Printing Factorizable Match Patterns
 
-When several patterns share the same right-hand side, it is additionally
-possible to share the clauses using disjunctive patterns. Assuming that the
-printing matching mode is on, this option (on by default) tells |Coq|'s
-printer to try to do this kind of factorization.
+   When several patterns share the same right-hand side, it is additionally
+   possible to share the clauses using disjunctive patterns. Assuming that the
+   printing matching mode is on, this option (on by default) tells |Coq|'s
+   printer to try to do this kind of factorization.
 
 Use of a default clause
 +++++++++++++++++++++++
 
-.. opt:: Printing Allow Default Clause
+.. flag:: Printing Allow Match Default Clause
 
-When several patterns share the same right-hand side which do not depend on the
-arguments of the patterns, yet an extra factorization is possible: the
-disjunction of patterns can be replaced with a `_` default clause. Assuming that
-the printing matching mode and the factorization mode are on, this option (on by
-default) tells |Coq|'s printer to use a default clause when relevant.
+   When several patterns share the same right-hand side which do not depend on the
+   arguments of the patterns, yet an extra factorization is possible: the
+   disjunction of patterns can be replaced with a `_` default clause. Assuming that
+   the printing matching mode and the factorization mode are on, this option (on by
+   default) tells |Coq|'s printer to use a default clause when relevant.
 
 Printing of wildcard patterns
 ++++++++++++++++++++++++++++++
 
-.. opt:: Printing Wildcard
+.. flag:: Printing Wildcard
 
-Some variables in a pattern may not occur in the right-hand side of
-the pattern-matching clause. When this option is on (default), the
-variables having no occurrences in the right-hand side of the
-pattern-matching clause are just printed using the wildcard symbol
-“_”.
+   Some variables in a pattern may not occur in the right-hand side of
+   the pattern matching clause. When this option is on (default), the
+   variables having no occurrences in the right-hand side of the
+   pattern matching clause are just printed using the wildcard symbol
+   “_”.
 
 
 Printing of the elimination predicate
 +++++++++++++++++++++++++++++++++++++
 
-.. opt:: Printing Synth
+.. flag:: Printing Synth
 
-In most of the cases, the type of the result of a matched term is
-mechanically synthesizable. Especially, if the result type does not
-depend of the matched term. When this option is on (default),
-the result type is not printed when |Coq| knows that it can re-
-synthesize it.
+   In most of the cases, the type of the result of a matched term is
+   mechanically synthesizable. Especially, if the result type does not
+   depend of the matched term. When this option is on (default),
+   the result type is not printed when |Coq| knows that it can re-
+   synthesize it.
 
 
 Printing matching on irrefutable patterns
 ++++++++++++++++++++++++++++++++++++++++++
 
-If an inductive type has just one constructor, pattern-matching can be
+If an inductive type has just one constructor, pattern matching can be
 written using the first destructuring let syntax.
 
-.. cmd:: Add Printing Let @ident
-
-   This adds `ident` to the list of inductive types for which pattern-matching
-   is written using a let expression.
-
-.. cmd:: Remove Printing Let @ident
-
-   This removes ident from this list. Note that removing an inductive
-   type from this list has an impact only for pattern-matching written
-   using :g:`match`. Pattern-matching explicitly written using a destructuring
-   :g:`let` are not impacted.
-
-.. cmd:: Test Printing Let for @ident
-
-   This tells if `ident` belongs to the list.
-
-.. cmd:: Print Table Printing Let
-
-   This prints the list of inductive types for which pattern-matching is
-   written using a let expression.
+.. table:: Printing Let @qualid
+   :name: Printing Let
 
-   The list of inductive types for which pattern-matching is written
-   using a :g:`let` expression is managed synchronously. This means that it is
-   sensitive to the command ``Reset``.
+   Specifies a set of qualids for which pattern matching is displayed using a let expression.
+   Note that this only applies to pattern matching instances entered with :g:`match`.
+   It doesn't affect pattern matching explicitly entered with a destructuring
+   :g:`let`.
+   Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set.
 
 
 Printing matching on booleans
 +++++++++++++++++++++++++++++
 
-If an inductive type is isomorphic to the boolean type, pattern-matching
-can be written using ``if`` … ``then`` … ``else`` …:
+If an inductive type is isomorphic to the boolean type, pattern matching
+can be written using ``if`` … ``then`` … ``else`` ….  This table controls
+which types are written this way:
 
-.. cmd:: Add Printing If @ident
+.. table:: Printing If @qualid
+   :name: Printing If
 
-   This adds ident to the list of inductive types for which pattern-matching is
-   written using an if expression.
-
-.. cmd:: Remove Printing If @ident
-
-   This removes ident from this list.
-
-.. cmd:: Test Printing If for @ident
-
-   This tells if ident belongs to the list.
-
-.. cmd:: Print Table Printing If
-
-   This prints the list of inductive types for which pattern-matching is
-   written using an if expression.
-
-The list of inductive types for which pattern-matching is written
-using an ``if`` expression is managed synchronously. This means that it is
-sensitive to the command ``Reset``.
+   Specifies a set of qualids for which pattern matching is displayed using
+   ``if`` … ``then`` … ``else`` ….  Use the :cmd:`Add @table` and :cmd:`Remove @table`
+   commands to update this set.
 
 This example emphasizes what the printing options offer.
 
@@ -674,7 +650,7 @@ than like this:
 
 *Limitations*
 
-|term_0| must be built as a *pure pattern-matching tree* (:g:`match … with`)
+|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`)
 with applications only *at the end* of each branch.
 
 Function does not support partial application of the function being
@@ -702,7 +678,7 @@ terminating functions.
 
     - the definition uses pattern matching on dependent types,
       which ``Function`` cannot deal with yet.
-    - the definition is not a *pattern-matching tree* as explained above.
+    - the definition is not a *pattern matching tree* as explained above.
 
 .. warn:: Cannot define principle(s) for @ident.
 
@@ -1240,7 +1216,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
 
    Prints the module type corresponding to :n:`@ident`.
 
-.. opt:: Short Module Printing
+.. flag:: Short Module Printing
 
    This option (off by default) disables the printing of the types of fields,
    leaving only their names, for the commands :cmd:`Print Module` and
@@ -1515,7 +1491,7 @@ says that the implicit argument is maximally inserted.
 
 Each implicit argument can be declared to have to be inserted maximally or non
 maximally. This can be governed argument per argument by the command
-:cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option.
+:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` option.
 
 .. seealso:: :ref:`displaying-implicit-args`.
 
@@ -1747,65 +1723,65 @@ appear strictly in the body of the type, they are implicit.
 Mode for automatic declaration of implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Implicit Arguments
+.. flag:: Implicit Arguments
 
-This option (off by default) allows to systematically declare implicit
-the arguments detectable as such. Auto-detection of implicit arguments is
-governed by options controlling whether strict and contextual implicit
-arguments have to be considered or not.
+   This option (off by default) allows to systematically declare implicit
+   the arguments detectable as such. Auto-detection of implicit arguments is
+   governed by options controlling whether strict and contextual implicit
+   arguments have to be considered or not.
 
 .. _controlling-strict-implicit-args:
 
 Controlling strict implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Strict Implicit
+.. flag:: Strict Implicit
 
-When the mode for automatic declaration of implicit arguments is on,
-the default is to automatically set implicit only the strict implicit
-arguments plus, for historical reasons, a small subset of the non-strict
-implicit arguments. To relax this constraint and to set
-implicit all non strict implicit arguments by default, you can turn this
-option off.
+   When the mode for automatic declaration of implicit arguments is on,
+   the default is to automatically set implicit only the strict implicit
+   arguments plus, for historical reasons, a small subset of the non-strict
+   implicit arguments. To relax this constraint and to set
+   implicit all non strict implicit arguments by default, you can turn this
+   option off.
 
-.. opt:: Strongly Strict Implicit
+.. flag:: Strongly Strict Implicit
 
-Use this option (off by default) to capture exactly the strict implicit
-arguments and no more than the strict implicit arguments.
+   Use this option (off by default) to capture exactly the strict implicit
+   arguments and no more than the strict implicit arguments.
 
 .. _controlling-contextual-implicit-args:
 
 Controlling contextual implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Contextual Implicit
+.. flag:: Contextual Implicit
 
-By default, |Coq| does not automatically set implicit the contextual
-implicit arguments. You can turn this option on to tell |Coq| to also
-infer contextual implicit argument.
+   By default, |Coq| does not automatically set implicit the contextual
+   implicit arguments. You can turn this option on to tell |Coq| to also
+   infer contextual implicit argument.
 
 .. _controlling-rev-pattern-implicit-args:
 
 Controlling reversible-pattern implicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Reversible Pattern Implicit
+.. flag:: Reversible Pattern Implicit
 
-By default, |Coq| does not automatically set implicit the reversible-pattern
-implicit arguments. You can turn this option on to tell |Coq| to also infer
-reversible-pattern implicit argument.
+   By default, |Coq| does not automatically set implicit the reversible-pattern
+   implicit arguments. You can turn this option on to tell |Coq| to also infer
+   reversible-pattern implicit argument.
 
 .. _controlling-insertion-implicit-args:
 
 Controlling the insertion of implicit arguments not followed by explicit arguments
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Maximal Implicit Insertion
+.. flag:: Maximal Implicit Insertion
 
-Assuming the implicit argument mode is on, this option (off by default)
-declares implicit arguments to be automatically inserted when a
-function is partially applied and the next argument of the function is
-an implicit one.
+   Assuming the implicit argument mode is on, this option (off by default)
+   declares implicit arguments to be automatically inserted when a
+   function is partially applied and the next argument of the function is
+   an implicit one.
 
 .. _explicit-applications:
 
@@ -1877,20 +1853,20 @@ if each of them is to be used maximally or not, use the command
 Explicit displaying of implicit arguments for pretty-printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Printing Implicit
+.. flag:: Printing Implicit
 
-By default, the basic pretty-printing rules hide the inferable implicit
-arguments of an application. Turn this option on to force printing all
-implicit arguments.
+   By default, the basic pretty-printing rules hide the inferable implicit
+   arguments of an application. Turn this option on to force printing all
+   implicit arguments.
 
-.. opt:: Printing Implicit Defensive
+.. flag:: Printing Implicit Defensive
 
-By default, the basic pretty-printing rules display the implicit
-arguments that are not detected as strict implicit arguments. This
-“defensive” mode can quickly make the display cumbersome so this can
-be deactivated by turning this option off.
+   By default, the basic pretty-printing rules display the implicit
+   arguments that are not detected as strict implicit arguments. This
+   “defensive” mode can quickly make the display cumbersome so this can
+   be deactivated by turning this option off.
 
-.. seealso:: :opt:`Printing All`.
+.. seealso:: :flag:`Printing All`.
 
 Interaction with subtyping
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1915,14 +1891,14 @@ but succeeds in
 Deactivation of implicit arguments for parsing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Parsing Explicit
+.. flag:: Parsing Explicit
 
-Turning this option on (it is off by default) deactivates the use of implicit arguments.
+   Turning this option on (it is off by default) deactivates the use of implicit arguments.
 
-In this case, all arguments of constants, inductive types,
-constructors, etc, including the arguments declared as implicit, have
-to be given as if no arguments were implicit. By symmetry, this also
-affects printing.
+   In this case, all arguments of constants, inductive types,
+   constructors, etc, including the arguments declared as implicit, have
+   to be given as if no arguments were implicit. By symmetry, this also
+   affects printing.
 
 Canonical structures
 ~~~~~~~~~~~~~~~~~~~~
@@ -2134,32 +2110,32 @@ to coercions are provided in :ref:`implicitcoercions`.
 Printing constructions in full
 ------------------------------
 
-.. opt:: Printing All
+.. flag:: Printing All
 
-Coercions, implicit arguments, the type of pattern-matching, but also
-notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some
-tactics (typically the tactics applying to occurrences of subterms are
-sensitive to the implicit arguments). Turning this option on
-deactivates all high-level printing features such as coercions,
-implicit arguments, returned type of pattern-matching, notations and
-various syntactic sugar for pattern-matching or record projections.
-Otherwise said, :opt:`Printing All` includes the effects of the options
-:opt:`Printing Implicit`, :opt:`Printing Coercions`, :opt:`Printing Synth`,
-:opt:`Printing Projections`, and :opt:`Printing Notations`. To reactivate
-the high-level printing features, use the command ``Unset Printing All``.
+   Coercions, implicit arguments, the type of pattern matching, but also
+   notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some
+   tactics (typically the tactics applying to occurrences of subterms are
+   sensitive to the implicit arguments). Turning this option on
+   deactivates all high-level printing features such as coercions,
+   implicit arguments, returned type of pattern matching, notations and
+   various syntactic sugar for pattern matching or record projections.
+   Otherwise said, :flag:`Printing All` includes the effects of the options
+   :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`,
+   :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate
+   the high-level printing features, use the command ``Unset Printing All``.
 
 .. _printing-universes:
 
 Printing universes
 ------------------
 
-.. opt:: Printing Universes
+.. flag:: Printing Universes
 
-Turn this option on to activate the display of the actual level of each
-occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in
-combination with :opt:`Printing All` can help to diagnose failures to unify
-terms apparently identical but internally different in the Calculus of Inductive
-Constructions.
+   Turn this option on to activate the display of the actual level of each
+   occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in
+   combination with :flag:`Printing All` can help to diagnose failures to unify
+   terms apparently identical but internally different in the Calculus of Inductive
+   Constructions.
 
 The constraints on the internal level of the occurrences of Type
 (see :ref:`Sorts`) can be printed using the command
@@ -2221,7 +2197,7 @@ form
 
 is appending to its name, indicating how the variables of its defining context are instantiated.
 The variables of the context of the existential variables which are
-instantiated by themselves are not written, unless the flag ``Printing Existential Instances``
+instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances`
 is on (see Section :ref:`explicit-display-existentials`), and this is why an
 existential variable used in the same context as its context of definition is written with no instance.
 
@@ -2243,11 +2219,11 @@ with a named-goal selector, see :ref:`goal-selectors`).
 Explicit displaying of existential instances for pretty-printing
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Printing Existential Instances
+.. flag:: Printing Existential Instances
 
-This option (off by default) activates the full display of how the
-context of an existential variable is instantiated at each of the
-occurrences of the existential variable.
+   This option (off by default) activates the full display of how the
+   context of an existential variable is instantiated at each of the
+   occurrences of the existential variable.
 
 .. _tactics-in-terms:
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index ad7b5c82fd..daf34500bf 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -374,13 +374,13 @@ Definition by case analysis
 ---------------------------
 
 Objects of inductive types can be destructurated by a case-analysis
-construction called *pattern-matching* expression. A pattern-matching
+construction called *pattern matching* expression. A pattern matching
 expression is used to analyze the structure of an inductive object and
 to apply specific treatments accordingly.
 
-This paragraph describes the basic form of pattern-matching. See
+This paragraph describes the basic form of pattern matching. See
 Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
-of the general form. The basic form of pattern-matching is characterized
+of the general form. The basic form of pattern matching is characterized
 by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a
 single :token:`pattern` and :token:`pattern` restricted to the form
 :n:`@qualid {* @ident}`.
@@ -388,9 +388,9 @@ single :token:`pattern` and :token:`pattern` restricted to the form
 The expression match ":token:`term`:math:`_0` :token:`return_type` with
 :token:`pattern`:math:`_1` => :token:`term`:math:`_1` :math:`|` … :math:`|`
 :token:`pattern`:math:`_n` => :token:`term`:math:`_n` end" denotes a
-*pattern-matching* over the term :token:`term`:math:`_0` (expected to be
+*pattern matching* over the term :token:`term`:math:`_0` (expected to be
 of an inductive type :math:`I`). The terms :token:`term`:math:`_1`\ …\
-:token:`term`:math:`_n` are the *branches* of the pattern-matching
+:token:`term`:math:`_n` are the *branches* of the pattern matching
 expression. Each of :token:`pattern`:math:`_i` has a form :token:`qualid`
 :token:`ident` where :token:`qualid` must denote a constructor. There should be
 exactly one branch for every constructor of :math:`I`.
@@ -403,7 +403,7 @@ inferred from the type of the branches [2]_.
 
 In the *dependent* case, there are three subcases. In the first subcase,
 the type in each branch may depend on the exact value being matched in
-the branch. In this case, the whole pattern-matching itself depends on
+the branch. In this case, the whole pattern matching itself depends on
 the term being matched. This dependency of the term being matched in the
 return type is expressed with an “as :token:`ident`” clause where :token:`ident`
 is dependent in the return type. For instance, in the following example:
@@ -424,7 +424,7 @@ is dependent in the return type. For instance, in the following example:
 
 the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`"
 and ":g:`or (eq bool false true) (eq bool false false)`" while the whole
-pattern-matching expression has type ":g:`or (eq bool b true) (eq bool b false)`",
+pattern matching expression has type ":g:`or (eq bool b true) (eq bool b false)`",
 the identifier :g:`b` being used to represent the dependency.
 
 .. note::
@@ -447,7 +447,7 @@ as the equality predicate (see Section :ref:`coq-equality`),
 the order predicate on natural numbers or the type of lists of a given
 length (see Section :ref:`matching-dependent`). In this configuration, the
 type of each branch can depend on the type dependencies specific to the
-branch and the whole pattern-matching expression has a type determined
+branch and the whole pattern matching expression has a type determined
 by the specific dependencies in the type of the term being matched. This
 dependency of the return type in the annotations of the inductive type
 is expressed using a “:g:`in` :math:`I` :g:`_ … _` :token:`pattern`:math:`_1` …
@@ -476,13 +476,13 @@ For instance, in the following example:
 
 the type of the branch is :g:`eq A x x` because the third argument of
 :g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the
-type of the whole pattern-matching expression has type :g:`eq A y x` because the
+type of the whole pattern matching expression has type :g:`eq A y x` because the
 third argument of eq is y in the type of H. This dependency of the case analysis
 in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the
 return type.
 
 Finally, the third subcase is a combination of the first and second
-subcase. In particular, it only applies to pattern-matching on terms in
+subcase. In particular, it only applies to pattern matching on terms in
 a type with annotations. For this third subcase, both the clauses ``as`` and
 ``in`` are available.
 
@@ -943,7 +943,7 @@ Parametrized inductive types
      sort for the inductive definition and will produce a less convenient
      rule for case elimination.
 
-.. opt:: Uniform Inductive Parameters
+.. flag:: Uniform Inductive Parameters
 
      When this option is set (it is off by default),
      inductive definitions are abstracted over their parameters
@@ -980,7 +980,7 @@ Variants
    The :cmd:`Variant` command is identical to the :cmd:`Inductive` command, except
    that it disallows recursive definition of types (for instance, lists cannot
    be defined using :cmd:`Variant`). No induction scheme is generated for
-   this variant, unless option :opt:`Nonrecursive Elimination Schemes` is on.
+   this variant, unless option :flag:`Nonrecursive Elimination Schemes` is on.
 
    .. exn:: The @num th argument of @ident must be @ident in @type.
       :undocumented:
@@ -1126,7 +1126,7 @@ constructions.
 
 .. cmd:: Fixpoint @ident @binders {? {struct @ident} } {? : @type } := @term
 
-   This command allows defining functions by pattern-matching over inductive
+   This command allows defining functions by pattern matching over inductive
    objects using a fixed point construction. The meaning of this declaration is
    to define :token:`ident` a recursive function with arguments specified by
    the :token:`binders` such that :token:`ident` applied to arguments
@@ -1329,7 +1329,7 @@ Chapter :ref:`Tactics`. The basic assertion command is:
 
       You are asserting a new statement while already being in proof editing mode.
       This feature, called nested proofs, is disabled by default.
-      To activate it, turn option :opt:`Nested Proofs Allowed` on.
+      To activate it, turn option :flag:`Nested Proofs Allowed` on.
 
    .. cmdv:: Lemma @ident {? @binders } : @type
              Remark @ident {? @binders } : @type
@@ -1403,7 +1403,7 @@ using the keyword :cmd:`Qed`.
 .. note::
 
    #. Several statements can be simultaneously asserted provided option
-      :opt:`Nested Proofs Allowed` was turned on.
+      :flag:`Nested Proofs Allowed` was turned on.
 
    #. Not only other assertions but any vernacular command can be given
       while in the process of proving a given assertion. In this case, the
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 38fdf243fe..edd83b7cee 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -24,14 +24,14 @@ represent respectively the natural and integer numbers, the authorized
 identificators and qualified names, Coq terms and patterns and all the atomic
 tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is
 the same as that of terms, but it is extended with pattern matching
-metavariables. In :token:`cpattern`, a pattern-matching metavariable is
+metavariables. In :token:`cpattern`, a pattern matching metavariable is
 represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The
 notation :g:`_` can also be used to denote metavariable whose instance is
 irrelevant. In the notation :g:`?id`, the identifier allows us to keep
 instantiations and to make constraints whereas :g:`_` shows that we are not
-interested in what will be matched. On the right hand side of pattern-matching
+interested in what will be matched. On the right hand side of pattern matching
 clauses, the named metavariables are used without the question mark prefix. There
-is also a special notation for second-order pattern-matching problems: in an
+is also a special notation for second-order pattern matching problems: in an
 applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any
 complex expression with (possible) dependencies in the variables :g:`id1 … idn`
 and returns a functional term of the form :g:`fun id1 … idn => term`.
@@ -833,7 +833,7 @@ We can carry out pattern matching on terms with:
       matching subterm is tried. If no further subterm matches, the next clause
       is tried. Matching subterms are considered top-bottom and from left to
       right (with respect to the raw printing obtained by setting option
-      :opt:`Printing All`).
+      :flag:`Printing All`).
 
    .. example::
 
@@ -1187,6 +1187,7 @@ Info trace
    not printed.
 
    .. opt:: Info Level @num
+      :name: Info Level
 
       This option is an alternative to the :cmd:`Info` command.
 
@@ -1197,7 +1198,7 @@ Info trace
 Interactive debugger
 ~~~~~~~~~~~~~~~~~~~~
 
-.. opt:: Ltac Debug
+.. flag:: Ltac Debug
 
    This option governs the step-by-step debugger that comes with the |Ltac| interpreter
 
@@ -1225,7 +1226,7 @@ following:
 
 A non-interactive mode for the debugger is available via the option:
 
-.. opt:: Ltac Batch Debug
+.. flag:: Ltac Batch Debug
 
    This option has the effect of presenting a newline at every prompt, when
    the debugger is on. The debug log thus created, which does not require
@@ -1246,7 +1247,7 @@ indicates the time spent in a tactic depending on its calling context. Thus
 it allows to locate the part of a tactic definition that contains the
 performance issue.
 
-.. opt:: Ltac Profiling
+.. flag:: Ltac Profiling
 
    This option enables and disables the profiler.
 
@@ -1332,7 +1333,7 @@ performance issue.
    benchmarking purposes.
 
 You can also pass the ``-profile-ltac`` command line option to ``coqc``, which
-turns the :opt:`Ltac Profiling` option on at the beginning of each document,
+turns the :flag:`Ltac Profiling` option on at the beginning of each document,
 and performs a :cmd:`Show Ltac Profile` at the end.
 
 .. warning::
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 3c0577b8e4..4b1b7719c5 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -112,7 +112,7 @@ list of assertion commands is given in :ref:`Assertions`. The command
       Aborts the editing of the proof named :token:`ident` (in case you have
       nested proofs).
 
-      .. seealso:: :opt:`Nested Proofs Allowed`
+      .. seealso:: :flag:`Nested Proofs Allowed`
 
    .. cmdv:: Abort All
 
@@ -200,13 +200,14 @@ The following options modify the behavior of ``Proof using``.
 
 
 .. opt:: Default Proof Using "@expression"
+   :name: Default Proof Using
 
    Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default
    Proof Using "a b"`` will complete all ``Proof`` commands not followed by a
    ``using`` part with ``using a b``.
 
 
-.. opt:: Suggest Proof Using
+.. flag:: Suggest Proof Using
 
    When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not
    provide one.
@@ -453,6 +454,7 @@ The following example script illustrates all these features:
 Set Bullet Behavior
 ```````````````````
 .. opt:: Bullet Behavior  %( "None" %| "Strict Subproofs" %)
+   :name: Bullet Behavior
 
    This option controls the bullet behavior and can take two possible values:
 
@@ -585,6 +587,7 @@ Controlling the effect of proof editing commands
 
 
 .. opt:: Hyps Limit @num
+   :name: Hyps Limit
 
    This option controls the maximum number of hypotheses displayed in goals
    after the application of a tactic. All the hypotheses remain usable
@@ -593,7 +596,7 @@ Controlling the effect of proof editing commands
    available hypotheses.
 
 
-.. opt:: Automatic Introduction
+.. flag:: Automatic Introduction
 
    This option controls the way binders are handled
    in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the
@@ -605,7 +608,7 @@ Controlling the effect of proof editing commands
    has to be used to move the assumptions to the local context.
 
 
-.. opt:: Nested Proofs Allowed
+.. flag:: Nested Proofs Allowed
 
    When turned on (it is off by default), this option enables support for nested
    proofs: a new assertion command can be inserted before the current proof is
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.
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index b0b57d00a0..f99c539251 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -48,7 +48,8 @@ specified, the default selector is used.
      tactic_invocation : toplevel_selector : tactic.
                        : |tactic .
 
-.. opt:: Default Goal Selector @toplevel_selector
+.. opt:: Default Goal Selector "@toplevel_selector"
+   :name: Default Goal Selector
 
    This option controls the default selector, used when no selector is
    specified when applying a tactic. The initial value is 1, hence the
@@ -124,7 +125,7 @@ that occurrences have to be selected in the hypotheses named :token:`ident`.
 If no numbers are given for hypothesis :token:`ident`, then all the
 occurrences of :token:`term` in the hypothesis are selected. If numbers are
 given, they refer to occurrences of :token:`term` when the term is printed
-using option :opt:`Printing All`, counting from left to right. In particular,
+using option :flag:`Printing All`, counting from left to right. In particular,
 occurrences of :token:`term` in implicit arguments
 (see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are
 counted.
@@ -448,7 +449,7 @@ Applying theorems
    ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by
    setting the following option:
 
-.. opt:: Universal Lemma Under Conjunction
+.. flag:: Universal Lemma Under Conjunction
 
    This option, which preserves compatibility with versions of Coq prior to
    8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`).
@@ -473,7 +474,7 @@ Applying theorems
    :token:`ident`. Tuples are decomposed in a width-first left-to-right order
    (for instance if the type of :g:`H1` is :g:`A <-> B` and the type of
    :g:`H2` is :g:`A` then :g:`apply H1 in H2` transforms the type of :g:`H2`
-   into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern-matching
+   into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern matching
    with dependent types.
 
    .. exn:: Statement without assumptions.
@@ -852,7 +853,7 @@ Managing the local context
    so that all the arguments of the i-th constructors of the corresponding
    inductive type are introduced can be controlled with the following option:
 
-   .. opt:: Bracketing Last Introduction Pattern
+   .. flag:: Bracketing Last Introduction Pattern
 
       Force completion, if needed, when the last introduction pattern is a
       disjunctive or conjunctive pattern (on by default).
@@ -1295,7 +1296,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
 
    This is equivalent to :n:`generalize @term` but it generalizes only over the
    specified occurrences of :n:`@term` (counting from left to right on the
-   expression printed using option :opt:`Printing All`).
+   expression printed using option :flag:`Printing All`).
 
 .. tacv:: generalize @term as @ident
 
@@ -2038,14 +2039,14 @@ and an explanation of the underlying technique.
    to the number of new equalities. The original equality is erased if it
    corresponds to a hypothesis.
 
-   .. opt:: Structural Injection
+   .. flag:: Structural Injection
 
       This option ensure that :n:`injection @term` erases the original hypothesis
       and leaves the generated equalities in the context rather than putting them
       as antecedents of the current goal, as if giving :n:`injection @term as`
       (with an empty list of names). This option is off by default.
 
-   .. opt:: Keep Proof Equalities
+   .. flag:: Keep Proof Equalities
 
       By default, :tacn:`injection` only creates new equalities between :n:`@terms`
       whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special
@@ -2077,7 +2078,7 @@ and an explanation of the underlying technique.
    being processed. By default, no equalities are generated if they
    relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort
    :g:`Prop`). This behavior can be turned off by using the option
-   :opt`Keep Proof Equalities`.
+   :flag`Keep Proof Equalities`.
 
 .. tacv:: inversion @num
 
@@ -2587,7 +2588,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       context for which an equality of the form :n:`@ident = t` or :n:`t = @ident`
       or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``.
 
-   .. opt:: Regular Subst Tactic
+   .. flag:: Regular Subst Tactic
 
       This option controls the behavior of :tacn:`subst`. When it is
       activated (it is by default), :tacn:`subst` also deals with the following corner cases:
@@ -2722,7 +2723,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :math:`\beta` (reduction of functional application), :math:`\delta`
    (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`),
    :math:`\iota` (reduction of
-   pattern-matching over a constructed term, and unfolding of :g:`fix` and
+   pattern matching over a constructed term, and unfolding of :g:`fix` and
    :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the
    flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``,
    ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix``
@@ -2805,12 +2806,13 @@ the conversion in hypotheses :n:`{+ @ident}`.
    compilation cost is higher, so it is worth using only for intensive
    computations.
 
-   .. opt:: NativeCompute Profiling
+   .. flag:: NativeCompute Profiling
 
       On Linux, if you have the ``perf`` profiler installed, this option makes
       it possible to profile ``native_compute`` evaluations.
 
-   .. opt:: NativeCompute Profile Filename
+   .. opt:: NativeCompute Profile Filename @string
+      :name: NativeCompute Profile Filename
 
       This option specifies the profile output; the default is
       ``native_compute_profile.data``. The actual filename used
@@ -2821,7 +2823,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
       on the profile file to see the results. Consult the ``perf`` documentation
       for more details.
 
-.. opt:: Debug Cbv
+.. flag:: Debug Cbv
 
    This option makes :tacn:`cbv` (and its derivative :tacn:`compute`) print
    information about the constants it encounters and the unfolding decisions it
@@ -2988,7 +2990,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose
    head occurrence is :n:`@qualid` (or :n:`@string`).
 
-.. opt:: Debug RAKAM
+.. flag:: Debug RAKAM
 
    This option makes :tacn:`cbn` print various debugging information.
    ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine.
@@ -3195,10 +3197,11 @@ hints of the database named core.
 The following options enable printing of informative or debug information for
 the :tacn:`auto` and :tacn:`trivial` tactics:
 
-.. opt:: Info Auto
-.. opt:: Debug Auto
-.. opt:: Info Trivial
-.. opt:: Debug Trivial
+.. flag:: Info Auto
+          Debug Auto
+          Info Trivial
+          Debug Trivial
+   :undocumented:
 
 .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
@@ -3228,8 +3231,9 @@ Note that ``ex_intro`` should be declared as a hint.
 
 :tacn:`eauto` also obeys the following options:
 
-.. opt:: Info Eauto
-.. opt:: Debug Eauto
+.. flag:: Info Eauto
+          Debug Eauto
+          :undocumented:
 
 .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>`
 
@@ -3563,7 +3567,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
    .. note::
 
-      One can use an ``Extern`` hint with no pattern to do pattern-matching on
+      One can use an ``Extern`` hint with no pattern to do pattern matching on
       hypotheses using ``match goal`` with inside the tactic.
 
 
@@ -3859,7 +3863,7 @@ some incompatibilities.
    ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive
    types with one constructor and no indices, i.e. record-style connectives.
 
-.. opt:: Intuition Negation Unfolding
+.. flag:: Intuition Negation Unfolding
 
    Controls whether :tacn:`intuition` unfolds inner negations which do not need
    to be unfolded. This option is on by default.
@@ -3888,6 +3892,7 @@ usual logical connectives but instead may reason about any first-order class
 inductive definition.
 
 .. opt:: Firstorder Solver @tactic
+   :name: Firstorder Solver
 
    The default tactic used by :tacn:`firstorder` when no rule applies is
    :g:`auto with *`, it can be reset locally or globally using this option.
@@ -3916,6 +3921,7 @@ inductive definition.
   This combines the effects of the different variants of :tacn:`firstorder`.
 
 .. opt:: Firstorder Depth @num
+   :name: Firstorder Depth
 
    This option controls the proof-search depth bound.
 
@@ -3978,7 +3984,7 @@ match against it.
   additional arguments can be given to congruence by filling in the holes in the
   terms given in the error message, using the :tacn:`congruence with` variant described above.
 
-.. opt:: Congruence Verbose
+.. flag:: Congruence Verbose
 
   This option makes :tacn:`congruence` print debug information.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 56df535d85..837d3f10a2 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -75,145 +75,106 @@ Displaying
 Flags, Options and Tables
 -----------------------------
 
-|Coq| configurability is based on flags (e.g. :opt:`Printing All`), options
-(e.g. :opt:`Printing Width`), or tables (e.g. :cmd:`Add Printing Record`). The
-names of flags, options and tables are made of non-empty sequences of
-identifiers (conventionally with capital initial letter). The general commands
-handling flags, options and tables are given below.
+Coq has many settings to control its behavior.  Setting types include flags, options
+and tables:
 
-.. TODO : flag is not a syntax entry
+* A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`.
+* An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`.
+* A :production:`table` contains a set of strings or qualids.
+* In addition, some commands provide settings, such as :cmd:`Extraction Language OCaml`.
 
-.. cmd:: Set @flag
+.. FIXME Convert `Extraction Language OCaml` to an option.
 
-   This command switches :n:`@flag` on. The original state of :n:`@flag`
-   is restored when the current module ends.
+Flags, options and tables are identified by a series of identifiers, each with an initial
+capital letter.
 
-   .. cmdv:: Local Set @flag
+.. cmd::  {? Local | Global | Export } Set @flag
+   :name: Set
 
-      This command switches :n:`@flag` on. The original state
-      of :n:`@flag` is restored when the current *section* ends.
+   Sets :token:`flag` on. Scoping qualifiers are
+   described :ref:`here <set_unset_scope_qualifiers>`.
 
-   .. cmdv:: Global Set @flag
-
-      This command switches :n:`@flag` on. The original state
-      of :n:`@flag` is *not* restored at the end of the module. Additionally, if
-      set in a file, :n:`@flag` is switched on when the file is `Require`-d.
-
-   .. cmdv:: Export Set @flag
-
-      This command switches :n:`@flag` on. The original state
-      of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
-      is switched on when this module is imported.
-
-
-.. cmd:: Unset @flag
-
-   This command switches :n:`@flag` off. The original state of
-   :n:`@flag` is restored when the current module ends.
-
-   .. cmdv:: Local Unset @flag
-
-      This command switches :n:`@flag` off. The original
-      state of :n:`@flag` is restored when the current *section* ends.
-
-   .. cmdv:: Global Unset @flag
-
-      This command switches :n:`@flag` off. The original
-      state of :n:`@flag` is *not* restored at the end of the module. Additionally,
-      if set in a file, :n:`@flag` is switched off when the file is `Require`-d.
-
-   .. cmdv:: Export Unset @flag
-
-      This command switches :n:`@flag` off. The original state
-      of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
-      is switched off when this module is imported.
+.. cmd:: {? Local | Global | Export } Unset @flag
+   :name: Unset
 
+   Sets :token:`flag` off. Scoping qualifiers are
+   described :ref:`here <set_unset_scope_qualifiers>`.
 
 .. cmd:: Test @flag
 
-   This command prints whether :n:`@flag` is on or off.
-
-
-.. cmd:: Set @option @value
+   Prints the current value of :token:`flag`.
 
-   This command sets :n:`@option` to :n:`@value`. The original value of ` option` is
-   restored when the current module ends.
 
-   .. TODO : option and value are not syntax entries
+.. cmd:: {? Local | Global | Export } Set @option ( @num | @string )
+   :name: Set @option
 
-   .. cmdv:: Local Set @option @value
+   Sets :token:`option` to the specified value.  Scoping qualifiers are
+   described :ref:`here <set_unset_scope_qualifiers>`.
 
-      This command sets :n:`@option` to :n:`@value`. The
-      original value of :n:`@option` is restored at the end of the module.
+.. cmd:: {? Local | Global | Export } Unset @option
+   :name: Unset @option
 
-   .. cmdv:: Global Set @option @value
+   Sets :token:`option` to its default value.  Scoping qualifiers are
+   described :ref:`here <set_unset_scope_qualifiers>`.
 
-      This command sets :n:`@option` to :n:`@value`. The
-      original value of :n:`@option` is *not* restored at the end of the module.
-      Additionally, if set in a file, :n:`@option` is set to value when the file
-      is `Require`-d.
-
-   .. cmdv:: Export Set @option
-
-      This command set :n:`@option` to :n:`@value`. The original state
-      of :n:`@option` is restored at the end of the current module, but :n:`@option`
-      is set to :n:`@value` when this module is imported.
-
-
-.. cmd:: Unset @option
-
-   This command turns off :n:`@option`.
-
-   .. cmdv:: Local Unset @option
+.. cmd:: Test @option
 
-      This command turns off :n:`@option`. The original state of :n:`@option`
-      is restored when the current *section* ends.
+   Prints the current value of :token:`option`.
 
-   .. cmdv:: Global Unset @option
+.. cmd:: Print Options
 
-      This command turns off :n:`@option`. The original state of :n:`@option`
-      is *not* restored at the end of the module. Additionally, if unset in a file,
-      :n:`@option` is reset to its default value when the file is `Require`-d.
+   Prints the current value of all flags and options, and the names of all tables.
 
-   .. cmdv:: Export Unset @option
 
-      This command turns off :n:`@option`. The original state of :n:`@option`
-      is restored at the end of the current module, but :n:`@option` is set to
-      its default value when this module is imported.
+.. cmd:: Add @table ( @string | @qualid )
+   :name: Add @table
 
+   Adds the specified value to :token:`table`.
 
-.. cmd:: Test @option
+.. cmd:: Remove @table ( @string | @qualid )
+   :name: Remove @table
 
-   This command prints the current value of :n:`@option`.
+   Removes the specified value from :token:`table`.
 
+.. cmd:: Test @table for ( @string | @qualid )
+   :name: Test @table for
 
-.. TODO : table is not a syntax entry
+   Reports whether :token:`table` contains the specified value.
 
-.. cmd:: Add @table @value
-   :name: Add `table` `value`
+.. cmd:: Print Table @table
+   :name: Print Table @table
 
-.. cmd:: Remove @table @value
-   :name: Remove `table` `value`
+   Prints the values in :token:`table`.
 
-.. cmd:: Test @table @value
-   :name: Test `table` `value`
+.. cmd:: Test @table
 
-.. cmd:: Test @table for @value
-   :name: Test `table` for `value`
+   A synonym for :cmd:`Print Table @table`.
 
-.. cmd:: Print Table @table
+.. cmd:: Print Tables
 
-These are general commands for tables.
+   A synonym for :cmd:`Print Options`.
 
+.. _set_unset_scope_qualifiers:
 
-.. cmd:: Print Options
+Scope qualifiers for :cmd:`Set` and :cmd:`Unset`
+`````````````````````````````````````````````````
 
-   This command lists all available flags, options and tables.
+:n:`{? Local | Global | Export }`
 
-   .. cmdv:: Print Tables
+Flag and option settings can be global in scope or local to nested scopes created by
+:cmd:`Module` and :cmd:`Section` commands.  There are four alternatives:
 
-      This is a synonymous of :cmd:`Print Options`.
+* no qualifier: the original setting is *not* restored at the end of the current module or section.
+* **Local**: the setting is applied within the current scope.  The original value of the option
+  or flag is restored at the end of the current module or section.
+* **Global**: similar to no qualifier, the original setting is *not* restored at the end of the current
+  module or section.  In addition, if the value is set in a file, then :cmd:`Require`-ing
+  the file sets the option.
+* **Export**: similar to **Local**, the original value of the option or flag is restored at the
+  end of the current module or section.  In addition, if the value is set in a file, then :cmd:`Import`-ing
+  the file sets the option.
 
+Newly opened scopes inherit the current settings.
 
 .. _requests-to-the-environment:
 
@@ -499,19 +460,16 @@ Requests to the environment
 
 .. note::
 
-   .. cmd:: Add Search Blacklist @string
+   .. table:: Search Blacklist @string
 
-      For the ``Search``, ``SearchHead``, ``SearchPattern`` and ``SearchRewrite``
-      queries, it is possible to globally filter the search results using this
-      command. A lemma whose fully-qualified name
-      contains any of the declared strings will be removed from the
-      search results. The default blacklisted substrings are ``_subproof`` and
+      Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`,
+      :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries.  A lemma whose
+      fully-qualified name contains any of the strings will be excluded from the
+      search results.  The default blacklisted substrings are ``_subterm``, ``_subproof`` and
       ``Private_``.
 
-   .. cmd:: Remove Search Blacklist @string
-
-      This command allows expunging this blacklist.
-
+      Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of
+      blacklisted strings.
 
 .. cmd:: Locate @qualid
 
@@ -976,6 +934,7 @@ Quitting and debugging
    displayed.
 
    .. opt:: Default Timeout @num
+      :name: Default Timeout
 
       This option controls a default timeout for subsequent commands, as if they
       were passed to a :cmd:`Timeout` command. Commands already starting by a
@@ -1000,11 +959,12 @@ Quitting and debugging
 Controlling display
 -----------------------
 
-.. opt:: Silent
+.. flag:: Silent
 
    This option controls the normal displaying.
 
 .. opt:: Warnings "{+, {? %( - %| + %) } @ident }"
+   :name: Warnings
 
    This option configures the display of warnings. It is experimental, and
    expects, between quotes, a comma-separated list of warning names or
@@ -1014,7 +974,7 @@ Controlling display
    interpreted from left to right, so in case of an overlap, the flags on the
    right have higher priority, meaning that `A,-A` is equivalent to `-A`.
 
-.. opt:: Search Output Name Only
+.. flag:: Search Output Name Only
 
    This option restricts the output of search commands to identifier names;
    turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`,
@@ -1035,7 +995,7 @@ Controlling display
    printing. Beyond this depth, display of subterms is replaced by dots. At the
    time of writing this documentation, the default value is 50.
 
-.. opt:: Printing Compact Contexts
+.. flag:: Printing Compact Contexts
 
    This option controls the compact display mode for goals contexts. When on,
    the printer tries to reduce the vertical size of goals contexts by putting
@@ -1043,13 +1003,13 @@ Controlling display
    does not exceed the printing width (see :opt:`Printing Width`). At the time
    of writing this documentation, it is off by default.
 
-.. opt:: Printing Unfocused
+.. flag:: Printing Unfocused
 
    This option controls whether unfocused goals are displayed. Such goals are
    created by focusing other goals with bullets (see :ref:`bullets` or
    :ref:`curly braces <curly-braces>`). It is off by default.
 
-.. opt:: Printing Dependent Evars Line
+.. flag:: Printing Dependent Evars Line
 
    This option controls the printing of the “(dependent evars: …)” line when
    ``-emacs`` is passed.
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:
author	Jim Fehrle	2018-09-01 12:39:09 -0700
committer	Jim Fehrle	2018-09-20 18:27:08 -0700
commit	ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 (patch)
tree	2f73dd477ac9276ba8ed9409aab613370d29c7fb /doc
parent	d4b5de427d94d82f09d58e0f1095f052a5900914 (diff)