Replace "option" in doc when it refers to a flag

19 files changed, 116 insertions, 115 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 3dc8707a34..9f92fc4c56 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -127,20 +127,21 @@ Concerning Haskell, type-preserving optimizations are less useful
 because of laziness. We still make some optimizations, for example in
 order to produce more readable code.
 
-The type-preserving optimizations are controlled by the following |Coq| options:
+The type-preserving optimizations are controlled by the following |Coq| flags
+and commands:
 
 .. 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
+   simplifications on Cases, etc). Turn this flag off if you want a
    ML term as close as possible to the Coq term.
 
 .. 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
-   types). Turn this option on to make sure that ``e:t``
+   types). Turn this flag on to make sure that ``e:t``
    implies that ``e':t'`` where ``e'`` and ``t'`` are the extracted
    code of ``e`` and ``t`` respectively.
 
@@ -150,7 +151,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    produces a singleton type (i.e. a type with only one constructor, and
    only one argument to this constructor), the inductive structure is
    removed and this type is seen as an alias to the inner type.
-   The typical example is ``sig``. This option allows disabling this
+   The typical example is ``sig``. This flag allows disabling this
    optimization when one wishes to preserve the inductive structure of types.
 
 .. flag:: Extraction AutoInline
@@ -159,7 +160,7 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    some defined constants, according to some heuristics
    like size of bodies, uselessness of some arguments, etc.
    Those heuristics are not always perfect; if you want to disable
-   this feature, turn this option off.
+   this feature, turn this flag off.
 
 .. cmd:: Extraction Inline {+ @qualid }
 
@@ -223,11 +224,11 @@ principles of extraction (logical parts and types).
 When an actual extraction takes place, an error is normally raised if the
 :cmd:`Extraction Implicit` declarations cannot be honored, that is
 if any of the implicit arguments still occurs in the final code.
-This behavior can be relaxed via the following option:
+This behavior can be relaxed via the following flag:
 
 .. flag:: Extraction SafeImplicits
 
-   Default is on. When this option is off, a warning is emitted
+   Default is on. When this flag is off, a warning is emitted
    instead of an error if some implicit arguments still occur in the
    final code of an extraction. This way, the extracted code may be
    obtained nonetheless and reviewed manually to locate the source of the issue
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 7fee62179b..c3b197288f 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -274,7 +274,7 @@ Activating the Printing of Coercions
 
 .. flag:: Printing Coercions
 
-   When on, this option forces all the coercions to be printed.
+   When on, this flag forces all the coercions to be printed.
    By default, coercions are not printed.
 
 .. table:: Printing Coercion @qualid
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 4a691bde3a..cc19c8b6a9 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -31,21 +31,21 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
 
 .. flag:: Simplex
 
-   This option (set by default) instructs the decision procedures to
+   This flag (set by default) instructs the decision procedures to
    use the Simplex method for solving linear goals. If it is not set,
    the decision procedures are using Fourier elimination.
 
 .. flag:: Lia Cache
 
-   This option (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`
+   This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`
 
 .. flag:: Nia Cache
 
-   This option (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache`
+   This flag (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache`
 
 .. flag:: Nra Cache
 
-   This option (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache`
+   This flag (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache`
 
 
 The tactics solve propositional formulas parameterized by atomic
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index b008508bbc..650a444a16 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -119,21 +119,21 @@ Options
 
    .. deprecated:: 8.5
 
-   This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
+   This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It
    resets internal name counters to make executions of :tacn:`omega` independent.
 
 .. flag:: Omega UseLocalDefs
 
-   This option (on by default) allows :tacn:`omega` to use the bodies of local
+   This flag (on by default) allows :tacn:`omega` to use the bodies of local
    variables.
 
 .. flag:: Omega System
 
-   This option (off by default) activate the printing of debug information
+   This flag (off by default) activate the printing of debug information
 
 .. flag:: Omega Action
 
-   This option (off by default) activate the printing of debug information
+   This flag (off by default) activate the printing of debug information
 
 Technical data
 --------------
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index cdb7ea834f..35729d852d 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 flag :flag:`Suggest Proof Using` makes |Coq| suggest, when a ``Qed``
+The :flag:`Suggest Proof Using` flag 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 69e442f399..a17dca1693 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -78,7 +78,7 @@ operation (see :ref:`extendedpatternmatching`).
   also works with the previous mechanism.
 
 
-There are options to control the generation of equalities and
+There are flags to control the generation of equalities and
 coercions.
 
 .. flag:: Program Cases
@@ -86,13 +86,13 @@ coercions.
    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
+   of |Coq| (see :ref:`extendedpatternmatching`) when this flag is
    deactivated.
 
 .. 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
+   (the flag is on by default). Coercion of subset types and pairs is still
    active in this case.
 
 .. flag:: Program Mode
@@ -343,7 +343,7 @@ optional tactic is replaced by the default one if not specified.
 
    .. deprecated:: 8.7
 
-   This option (on by default) controls whether obligations should have
+   This flag (on by default) controls whether obligations should have
    their context minimized to the set of variables used in the proof of
    the obligation, to avoid unnecessary dependencies.
 
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index db3e20a9c6..1bbf988505 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -560,8 +560,8 @@ Settings
 
    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 to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this
-   option to 0 turns that option off.
+   of goals.  Setting this option to 1 or 2 turns on the :flag:`Typeclasses Debug` flag; setting this
+   option to 0 turns that flag off.
 
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 905068e316..7adb25cbd6 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -129,12 +129,12 @@ Polymorphic, Monomorphic
 
 .. flag:: Universe Polymorphism
 
-   Once enabled, this option will implicitly prepend ``Polymorphic`` to any
+   Once enabled, this flag will implicitly prepend ``Polymorphic`` to any
    definition of the user.
 
 .. cmd:: Monomorphic @definition
 
-   When the :flag:`Universe Polymorphism` option is set, to make a definition
+   When the :flag:`Universe Polymorphism` flag is set, to make a definition
    producing global universe constraints, one can use the ``Monomorphic`` prefix.
 
 Many other commands support the ``Polymorphic`` flag, including:
@@ -162,8 +162,8 @@ declared cumulative using the :g:`Cumulative` prefix.
 
    Declares the inductive as cumulative
 
-Alternatively, there is a flag :flag:`Polymorphic Inductive
-Cumulativity` which when set, makes all subsequent *polymorphic*
+Alternatively, there is a :flag:`Polymorphic Inductive
+Cumulativity` flag 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`
 prefix.
@@ -174,7 +174,7 @@ prefix.
 
 .. flag:: Polymorphic Inductive Cumulativity
 
-   When this option is on, it sets all following polymorphic inductive
+   When this flag is on, it sets all following polymorphic inductive
    types as cumulative (it is off by default).
 
 Consider the examples below.
@@ -222,8 +222,8 @@ Cumulative inductive types, coinductive 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 :flag:`Polymorphic Inductive Cumulativity`.
-That is, this option, when set, makes all subsequent *polymorphic*
+Notice that this is not the case for the :flag:`Polymorphic Inductive Cumulativity` flag.
+That is, this flag, 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.
 
@@ -439,7 +439,7 @@ underscore or by omitting the annotation to a polymorphic definition.
 
 .. flag:: Strict Universe Declaration
 
-   Turning this option off allows one to freely use
+   Turning this flag off allows one to freely use
    identifiers for universes without declaring them first, with the
    semantics that the first use declares it. In this mode, the universe
    names are not associated with the definition or proof once it has been
@@ -447,7 +447,7 @@ underscore or by omitting the annotation to a polymorphic definition.
 
 .. flag:: Private Polymorphic Universes
 
-   This option, on by default, removes universes which appear only in
+   This flag, on by default, removes universes which appear only in
    the body of an opaque polymorphic definition from the definition's
    universe arguments. As such, no value needs to be provided for
    these universes when instantiating the definition. Universe
@@ -480,7 +480,7 @@ underscore or by omitting the annotation to a polymorphic definition.
       About foo.
 
    To recover the same behaviour with regard to universes as
-   :g:`Defined`, the option :flag:`Private Polymorphic Universes` may
+   :g:`Defined`, the :flag:`Private Polymorphic Universes` flag may
    be unset:
 
    .. coqtop:: all
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 6410620b40..56b64eb5ab 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1195,7 +1195,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
 
 .. flag:: Auto Template Polymorphism
 
-   This option, enabled by default, makes every inductive type declared
+   This flag, enabled by default, makes every inductive type declared
    at level :math:`\Type` (without annotations or hiding it behind a
    definition) template polymorphic if possible.
 
@@ -1224,7 +1224,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
 
 .. flag:: Template Check
 
-   Unsetting option :flag:`Template Check` disables the check of
+   This flag is on by default. Turning it off disables the check of
    locality of the sorts when abstracting the inductive over its
    parameters. This is a deprecated and *unsafe* flag that can introduce
    inconsistencies, it is only meant to help users incrementally update
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 54669534c7..a047bab421 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -188,7 +188,7 @@ other arguments are the parameters of the inductive type.
 .. note:: Induction schemes are automatically generated for inductive records.
    Automatic generation of induction schemes for non-recursive records
    defined with the ``Record`` keyword can be activated with the
-   ``Nonrecursive Elimination Schemes`` option (see :ref:`proofschemes-induction-principles`).
+   :flag:`Nonrecursive Elimination Schemes` flag (see :ref:`proofschemes-induction-principles`).
 
 .. note:: ``Structure`` is a synonym of the keyword ``Record``.
 
@@ -243,14 +243,14 @@ Primitive Projections
 
 .. flag:: Printing Primitive Projection Parameters
 
-   This compatibility option reconstructs internally omitted parameters at
+   This compatibility flag reconstructs internally omitted parameters at
    printing time (even though they are absent in the actual AST manipulated
    by the kernel).
 
 Primitive Record Types
 ++++++++++++++++++++++
 
-When the :flag:`Primitive Projections` option is on, definitions of
+When the :flag:`Primitive Projections` flag 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.
@@ -302,7 +302,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 :flag:`Printing Primitive Projection Parameters` option
+projection if the :flag:`Printing Primitive Projection Parameters` flag
 is off: For a primitive projection application, parameters are printed
 as underscores while for the compatibility projections they are printed
 as usual.
@@ -481,7 +481,7 @@ Printing nested patterns
    pattern matching into a single pattern matching over a nested
    pattern.
 
-   When this option is on (default), |Coq|’s printer tries to do such
+   When this flag 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.
@@ -494,7 +494,7 @@ Factorization of clauses with same right-hand side
 
    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
+   printing matching mode is on, this flag (on by default) tells |Coq|'s
    printer to try to do this kind of factorization.
 
 Use of a default clause
@@ -505,7 +505,7 @@ Use of a 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
+   the printing matching mode and the factorization mode are on, this flag (on by
    default) tells |Coq|'s printer to use a default clause when relevant.
 
 Printing of wildcard patterns
@@ -514,7 +514,7 @@ Printing of wildcard patterns
 .. 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
+   the pattern matching clause. When this flag 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
    “_”.
@@ -527,7 +527,7 @@ Printing of the elimination predicate
 
    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),
+   depend of the matched term. When this flag is on (default),
    the result type is not printed when |Coq| knows that it can re-
    synthesize it.
 
@@ -562,7 +562,7 @@ which types are written this way:
    ``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.
+This example emphasizes what the printing settings offer.
 
 .. example::
 
@@ -1311,7 +1311,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
 
 .. flag:: Short Module Printing
 
-   This option (off by default) disables the printing of the types of fields,
+   This flag (off by default) disables the printing of the types of fields,
    leaving only their names, for the commands :cmd:`Print Module` and
    :cmd:`Print Module Type`.
 
@@ -1584,7 +1584,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 :flag:`Maximal Implicit Insertion` option.
+:cmd:`Arguments (implicits)` or globally by the :flag:`Maximal Implicit Insertion` flag.
 
 .. seealso:: :ref:`displaying-implicit-args`.
 
@@ -1757,7 +1757,7 @@ Automatic declaration of implicit arguments
    This command tells |Coq| to automatically detect what are the implicit arguments of a
    defined object.
 
-   The auto-detection is governed by options telling if strict,
+   The auto-detection is governed by flags telling if strict,
    contextual, or reversible-pattern implicit arguments must be
    considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`,
    :ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`).
@@ -1827,9 +1827,9 @@ Mode for automatic declaration of implicit arguments
 
 .. flag:: Implicit Arguments
 
-   This option (off by default) allows to systematically declare implicit
+   This flag (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
+   governed by flags controlling whether strict and contextual implicit
    arguments have to be considered or not.
 
 .. _controlling-strict-implicit-args:
@@ -1844,11 +1844,11 @@ Controlling strict implicit arguments
    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.
+   flag off.
 
 .. flag:: Strongly Strict Implicit
 
-   Use this option (off by default) to capture exactly the strict implicit
+   Use this flag (off by default) to capture exactly the strict implicit
    arguments and no more than the strict implicit arguments.
 
 .. _controlling-contextual-implicit-args:
@@ -1859,7 +1859,7 @@ Controlling contextual implicit arguments
 .. 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
+   implicit arguments. You can turn this flag on to tell |Coq| to also
    infer contextual implicit argument.
 
 .. _controlling-rev-pattern-implicit-args:
@@ -1870,7 +1870,7 @@ Controlling reversible-pattern implicit arguments
 .. 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
+   implicit arguments. You can turn this flag on to tell |Coq| to also infer
    reversible-pattern implicit argument.
 
 .. _controlling-insertion-implicit-args:
@@ -1880,7 +1880,7 @@ Controlling the insertion of implicit arguments not followed by explicit argumen
 
 .. flag:: Maximal Implicit Insertion
 
-   Assuming the implicit argument mode is on, this option (off by default)
+   Assuming the implicit argument mode is on, this flag (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.
@@ -1962,7 +1962,7 @@ Explicit displaying of implicit arguments for pretty-printing
 .. 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
+   arguments of an application. Turn this flag on to force printing all
    implicit arguments.
 
 .. flag:: Printing Implicit Defensive
@@ -1970,7 +1970,7 @@ Explicit displaying of implicit arguments for pretty-printing
    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.
+   be deactivated by turning this flag off.
 
 .. seealso:: :flag:`Printing All`.
 
@@ -1999,7 +1999,7 @@ Deactivation of implicit arguments for parsing
 
 .. flag:: Parsing Explicit
 
-   Turning this option on (it is off by default) deactivates the use of implicit arguments.
+   Turning this flag 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
@@ -2271,11 +2271,11 @@ Printing constructions in full
    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
+   sensitive to the implicit arguments). Turning this flag 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
+   Otherwise said, :flag:`Printing All` includes the effects of the flags
    :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``.
@@ -2287,8 +2287,8 @@ 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
+   Turn this flag on to activate the display of the actual level of each
+   occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard flag, 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.
@@ -2299,7 +2299,7 @@ Printing universes
    This command can be used to print the constraints on the internal level
    of the occurrences of :math:`\Type` (see :ref:`Sorts`).
 
-   If the optional ``Sorted`` option is given, each universe will be made
+   If the ``Sorted`` keyword is present, each universe will be made
    equivalent to a numbered label reflecting its level (with a linear
    ordering) in the universe hierarchy.
 
@@ -2357,7 +2357,7 @@ outside of its context of definition, its instance, written under the
 form :n:`{ {*; @ident := @term} }` 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 :flag:`Printing Existential Instances`
+instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag
 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.
 
@@ -2381,7 +2381,7 @@ Explicit displaying of existential instances for pretty-printing
 
 .. flag:: Printing Existential Instances
 
-   This option (off by default) activates the full display of how the
+   This flag (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.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index dd65d4aeb3..f667dd94b0 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -779,7 +779,7 @@ Simple inductive types
       The types of the constructors have to satisfy a *positivity condition*
       (see Section :ref:`positivity`). This condition ensures the soundness of
       the inductive definition. The positivity checking can be disabled using
-      the option :flag:`Positivity Checking` (see :ref:`controlling-typing-flags`).
+      the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
@@ -956,7 +956,7 @@ Parameterized inductive types
 
 .. flag:: Uniform Inductive Parameters
 
-     When this option is set (it is off by default),
+     When this flag is set (it is off by default),
      inductive definitions are abstracted over their parameters
      before type checking constructors, allowing to write:
 
@@ -991,7 +991,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 :flag:`Nonrecursive Elimination Schemes` is on.
+   this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on.
 
    .. exn:: The @num th argument of @ident must be @ident in @type.
       :undocumented:
@@ -1393,11 +1393,11 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       The name you provided is already defined. You have then to choose
       another name.
 
-   .. exn:: Nested proofs are not allowed unless you turn option Nested Proofs Allowed on.
+   .. exn:: Nested proofs are not allowed unless you turn the :flag:`Nested Proofs Allowed` flag on.
 
       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 :flag:`Nested Proofs Allowed` on.
+      To activate it, turn the :flag:`Nested Proofs Allowed` flag on.
 
    .. cmdv:: Lemma @ident {? @binders } : @type
              Remark @ident {? @binders } : @type
@@ -1470,8 +1470,8 @@ using the keyword :cmd:`Qed`.
 
 .. note::
 
-   #. Several statements can be simultaneously asserted provided option
-      :flag:`Nested Proofs Allowed` was turned on.
+   #. Several statements can be simultaneously asserted provided the
+      :flag:`Nested Proofs Allowed` flag 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/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 70259ff565..97e7af8cb4 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -36,7 +36,7 @@ toplevel with the command ``Coqloop.loop();;``.
 
 .. flag:: Coqtop Exit On Error
 
-   This option, off by default, causes coqtop to exit with status code
+   This flag, off by default, causes coqtop to exit with status code
    ``1`` if a command produces an error instead of recovering from it.
 
 Batch compilation (coqc)
@@ -219,7 +219,7 @@ and ``coqtop``, unless stated otherwise:
   .. warning:: This makes the logic inconsistent.
 :-mangle-names *ident*: *Experimental.* Do not depend on this option. Replace
   Coq's auto-generated name scheme with names of the form *ident0*, *ident1*,
-  etc. Within Coq, the flag :flag:`Mangle Names` turns this behavior on,
+  etc. Within Coq, the :flag:`Mangle Names` flag turns this behavior on,
   and the :opt:`Mangle Names Prefix` option sets the prefix to use. This feature
   is intended to be used as a linter for developments that want to be robust to
   changes in the auto-generated name scheme. The options are provided to
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 6efc634087..e37f300915 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -860,8 +860,8 @@ We can carry out pattern matching on terms with:
       If the evaluation of the right-hand-side of a valid match fails, the next
       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
-      :flag:`Printing All`).
+      right (with respect to the raw printing obtained by setting the
+      :flag:`Printing All` flag).
 
    .. example::
 
@@ -1642,7 +1642,7 @@ Interactive debugger
 
 .. flag:: Ltac Debug
 
-   This option governs the step-by-step debugger that comes with the |Ltac| interpreter.
+   This flag governs the step-by-step debugger that comes with the |Ltac| interpreter.
 
 When the debugger is activated, it stops at every step of the evaluation of
 the current |Ltac| expression and prints information on what it is doing.
@@ -1666,13 +1666,13 @@ following:
 .. exn:: Debug mode not available in the IDE
    :undocumented:
 
-A non-interactive mode for the debugger is available via the option:
+A non-interactive mode for the debugger is available via the flag:
 
 .. flag:: Ltac Batch Debug
 
-   This option has the effect of presenting a newline at every prompt, when
+   This flag has the effect of presenting a newline at every prompt, when
    the debugger is on. The debug log thus created, which does not require
-   user input to generate when this option is set, can then be run through
+   user input to generate when this flag is set, can then be run through
    external tools such as diff.
 
 Profiling |Ltac| tactics
@@ -1691,7 +1691,7 @@ performance issue.
 
 .. flag:: Ltac Profiling
 
-   This option enables and disables the profiler.
+   This flag enables and disables the profiler.
 
 .. cmd:: Show Ltac Profile
 
@@ -1775,7 +1775,7 @@ performance issue.
    benchmarking purposes.
 
 You can also pass the ``-profile-ltac`` command line option to ``coqc``, which
-turns the :flag:`Ltac Profiling` option on at the beginning of each document,
+turns the :flag:`Ltac Profiling` flag 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 00f8269dc3..6884b6e998 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -804,7 +804,7 @@ Controlling the effect of proof editing commands
 
 .. flag:: Nested Proofs Allowed
 
-   When turned on (it is off by default), this option enables support for nested
+   When turned on (it is off by default), this flag enables support for nested
    proofs: a new assertion command can be inserted before the current proof is
    finished, in which case Coq will temporarily switch to the proof of this
    *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed`
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 04d0503ff4..4c697be963 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2764,7 +2764,7 @@ typeclass inference.
 
 .. flag:: SsrHave NoTCResolution
 
-   This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses).
+   This flag restores the behavior of |SSR| 1.4 and below (never resolve typeclasses).
 
 Variants: the suff and wlog tactics
 ```````````````````````````````````
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 78753fc053..ad7f9af0f9 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -261,7 +261,7 @@ These patterns can be used when the hypothesis is an equality:
    conjunctive pattern that doesn't give enough simple patterns to match
    all the arguments in the constructor.  If set (the default), |Coq| generates
    additional names to match the number of arguments.
-   Unsetting the option will put the additional hypotheses in the goal instead, behavior that is more
+   Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more
    similar to |SSR|'s intro patterns.
 
    .. deprecated:: 8.10
@@ -477,7 +477,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 :flag:`Printing All`, counting from left to right. In particular,
+using the :flag:`Printing All` flag, counting from left to right. In particular,
 occurrences of :token:`term` in implicit arguments
 (see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are
 counted.
@@ -804,11 +804,11 @@ Applying theorems
    component of the tuple matches the goal, it excludes components whose
    statement would result in applying an universal lemma of the form
    ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by
-   setting the following option:
+   setting the following flag:
 
 .. flag:: Universal Lemma Under Conjunction
 
-   This option, which preserves compatibility with versions of Coq prior to
+   This flag, which preserves compatibility with versions of Coq prior to
    8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`).
 
 .. tacn:: apply @term in @ident
@@ -1527,7 +1527,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 :flag:`Printing All`).
+   expression printed using the :flag:`Printing All` flag).
 
 .. tacv:: generalize @term as @ident
 
@@ -2300,16 +2300,16 @@ and an explanation of the underlying technique.
 
    .. flag:: Structural Injection
 
-      This option ensure that :n:`injection @term` erases the original hypothesis
+      This flag ensures 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.
+      (with an empty list of names). This flag is off by default.
 
    .. flag:: Keep Proof Equalities
 
       By default, :tacn:`injection` only creates new equalities between :n:`@term`\s
       whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special
-      behavior for objects that are proofs of a statement in :g:`Prop`. This option
+      behavior for objects that are proofs of a statement in :g:`Prop`. This flag
       controls this behavior.
 
 .. tacn:: inversion @ident
@@ -2862,26 +2862,26 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
    .. flag:: Regular Subst Tactic
 
-      This option controls the behavior of :tacn:`subst`. When it is
+      This flag controls the behavior of :tacn:`subst`. When it is
       activated (it is by default), :tacn:`subst` also deals with the following corner cases:
 
       + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2`
         and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not
         a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u`
-        or :n:`u = @ident`:sub:`2`; without the option, a second call to
+        or :n:`u = @ident`:sub:`2`; without the flag, a second call to
         subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or
         `t′` respectively.
-      + The presence of a recursive equation which without the option would
+      + The presence of a recursive equation which without the flag would
         be a cause of failure of :tacn:`subst`.
       + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2`
         and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the
-        option would be a cause of failure of :tacn:`subst`.
+        flag would be a cause of failure of :tacn:`subst`.
 
       Additionally, it prevents a local definition such as :n:`@ident := t` to be
       unfolded which otherwise it would exceptionally unfold in configurations
       containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident`
       with `u′` not a variable. Finally, it preserves the initial order of
-      hypotheses, which without the option it may break.
+      hypotheses, which without the flag it may break.
       default.
 
 
@@ -3086,7 +3086,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    .. flag:: NativeCompute Profiling
 
-      On Linux, if you have the ``perf`` profiler installed, this option makes
+      On Linux, if you have the ``perf`` profiler installed, this flag makes
       it possible to profile :tacn:`native_compute` evaluations.
 
    .. opt:: NativeCompute Profile Filename @string
@@ -3103,7 +3103,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
 .. flag:: Debug Cbv
 
-   This option makes :tacn:`cbv` (and its derivative :tacn:`compute`) print
+   This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print
    information about the constants it encounters and the unfolding decisions it
    makes.
 
@@ -3271,7 +3271,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
 .. flag:: Debug RAKAM
 
-   This option makes :tacn:`cbn` print various debugging information.
+   This flag makes :tacn:`cbn` print various debugging information.
    ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine.
 
 .. tacn:: unfold @qualid
@@ -3548,7 +3548,7 @@ Automation
           Info Trivial
           Debug Trivial
 
-   These options enable printing of informative or debug information for
+   These flags enable printing of informative or debug information for
    the :tacn:`auto` and :tacn:`trivial` tactics.
 
 .. tacn:: eauto
@@ -3576,7 +3576,7 @@ Automation
 
       The various options for :tacn:`eauto` are the same as for :tacn:`auto`.
 
-   :tacn:`eauto` also obeys the following options:
+   :tacn:`eauto` also obeys the following flags:
 
    .. flag:: Info Eauto
              Debug Eauto
@@ -3720,7 +3720,7 @@ automatically created.
    .. cmdv:: Local Hint @hint_definition : {+ @ident}
 
       This is used to declare hints that must not be exported to the other modules
-      that require and import the current module. Inside a section, the option
+      that require and import the current module. Inside a section, the flag
       Local is useless since hints do not survive anyway to the closure of
       sections.
 
@@ -4196,7 +4196,7 @@ some incompatibilities.
 .. flag:: Intuition Negation Unfolding
 
    Controls whether :tacn:`intuition` unfolds inner negations which do not need
-   to be unfolded. This option is on by default.
+   to be unfolded. This flag is on by default.
 
 .. tacn:: rtauto
    :name: rtauto
@@ -4316,7 +4316,7 @@ some incompatibilities.
 
 .. flag:: Congruence Verbose
 
-  This option makes :tacn:`congruence` print debug information.
+  This flag makes :tacn:`congruence` print debug information.
 
 
 Checking properties of terms
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 843459b723..e87b76b4ab 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -962,7 +962,7 @@ Controlling display
 
 .. flag:: Silent
 
-   This option controls the normal displaying.
+   This flag controls the normal displaying.
 
 .. opt:: Warnings "{+, {? {| - | + } } @ident }"
    :name: Warnings
@@ -977,7 +977,7 @@ Controlling display
 
 .. flag:: Search Output Name Only
 
-   This option restricts the output of search commands to identifier names;
+   This flag restricts the output of search commands to identifier names;
    turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`,
    :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their
    output, printing only identifiers.
@@ -998,7 +998,7 @@ Controlling display
 
 .. flag:: Printing Compact Contexts
 
-   This option controls the compact display mode for goals contexts. When on,
+   This flag controls the compact display mode for goals contexts. When on,
    the printer tries to reduce the vertical size of goals contexts by putting
    several variables (even if of different types) on the same line provided it
    does not exceed the printing width (see :opt:`Printing Width`). At the time
@@ -1006,13 +1006,13 @@ Controlling display
 
 .. flag:: Printing Unfocused
 
-   This option controls whether unfocused goals are displayed. Such goals are
+   This flag 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.
 
 .. flag:: Printing Dependent Evars Line
 
-   This option controls the printing of the “(dependent evars: …)” information
+   This flag controls the printing of the “(dependent evars: …)” information
    after each tactic.  The information is used by the Prooftree tool in Proof
    General. (https://askra.de/software/prooftree)
 
@@ -1213,7 +1213,7 @@ Controlling Typing Flags
 
 .. flag:: Guard Checking
 
-   This option can be used to enable/disable the guard checking of
+   This flag can be used to enable/disable the guard checking of
    fixpoints. Warning: this can break the consistency of the system, use at your
    own risk. Decreasing argument can still be specified: the decrease is not checked
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
@@ -1221,14 +1221,14 @@ Controlling Typing Flags
 
 .. flag:: Positivity Checking
 
-   This option can be used to enable/disable the positivity checking of inductive
+   This flag can be used to enable/disable the positivity checking of inductive
    types and the productivity checking of coinductive types. Warning: this can
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
 .. flag:: Universe Checking
 
-   This option can be used to enable/disable the checking of universes, providing a
+   This flag can be used to enable/disable the checking of universes, providing a
    form of "type in type".  Warning: this breaks the consistency of the system, use
    at your own risk.  Constants relying on "type in type" are printed by
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 3a12ee288a..5b0b3c51b0 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -128,7 +128,7 @@ Automatic declaration of schemes
 
 .. warning::
 
-   You have to be careful with this option since Coq may now reject well-defined
+   You have to be careful with these flags since Coq may now reject well-defined
    inductive types because it cannot compute a Boolean equality for them.
 
 .. flag:: Rewriting Schemes
diff --git a/stm/stm.ml b/stm/stm.ml
index c399b69a77..2b68e1778d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2892,7 +2892,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
       | VtStartProof (guarantee, names) ->
 
          if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
-           "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
+           "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on."
            |> Pp.str
            |> (fun s -> (UserError (None, s), Exninfo.null))
            |> State.exn_on ~valid:Stateid.dummy newtip