diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 17 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 54 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 192 |
5 files changed, 126 insertions, 156 deletions
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. |