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

5 files changed, 39 insertions, 39 deletions

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