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

8 files changed, 34 insertions, 33 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