From db391451c5f89c034e6fec1b10fec66a25e3d4d4 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 4 Nov 2019 19:14:07 -0800 Subject: Replace "option" in doc when it refers to a flag --- doc/sphinx/proof-engine/ltac.rst | 16 ++++----- doc/sphinx/proof-engine/proof-handling.rst | 2 +- .../proof-engine/ssreflect-proof-language.rst | 2 +- doc/sphinx/proof-engine/tactics.rst | 42 +++++++++++----------- doc/sphinx/proof-engine/vernacular-commands.rst | 16 ++++----- 5 files changed, 39 insertions(+), 39 deletions(-) (limited to 'doc/sphinx/proof-engine') 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 `). 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 -- cgit v1.2.3