diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 17 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 109 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 22 |
6 files changed, 148 insertions, 73 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 79eddbd3b5..b2b426ada5 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -127,7 +127,7 @@ mode but it can also be used in toplevel definitions as shown below. : gfail [`natural`] [`message_token` ... `message_token`] : fresh [ `component` … `component` ] : context `ident` [`term`] - : eval `redexpr` in `term` + : eval `red_expr` in `term` : type of `term` : constr : `term` : uconstr : `term` @@ -516,7 +516,9 @@ Coq provides a derived tactic to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr :name: assert_fails - This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`. + This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and + behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr` + has at least one success. Checking the success ~~~~~~~~~~~~~~~~~~~~ @@ -528,7 +530,7 @@ success: :name: assert_succeeds This behaves like - :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. + :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`. Solving ~~~~~~~ @@ -858,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:: @@ -984,9 +986,9 @@ Computing in a constr Evaluation of a term can be performed with: -.. tacn:: eval @redexpr in @term +.. tacn:: eval @red_expr in @term - where :n:`@redexpr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`, + where :n:`@red_expr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`, :tacn:`compute`, :tacn:`simpl`, :tacn:`cbv`, :tacn:`lazy`, :tacn:`unfold`, :tacn:`fold`, :tacn:`pattern`. @@ -1640,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. @@ -1664,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 @@ -1689,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 @@ -1773,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/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 18d2c79461..dd80b29bda 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1,12 +1,12 @@ .. _ltac2: +Ltac2 +===== + .. coqtop:: none From Ltac2 Require Import Ltac2. -Ltac2 -===== - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: @@ -563,6 +563,20 @@ for it. - `&x` as a Coq constr expression expands to `ltac2:(Control.refine (fun () => hyp @x))`. +In the special case where Ltac2 antiquotations appear inside a Coq term +notation, the notation variables are systematically bound in the body +of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents +untyped syntactic Coq expressions, which can by typed in the +current context using the `Ltac2.Constr.pretype` function. + +.. example:: + + The following notation is essentially the identity. + + .. coqtop:: in + + Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing). + Dynamic semantics ***************** diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 57a54bc0ad..6884b6e998 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,7 +535,7 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof Displays the proof term generated by the tactics @@ -544,6 +544,12 @@ Requesting information constructed. Each hole is an existential variable, which appears as a question mark followed by an identifier. + Experimental: Specifying “Diffs” highlights the difference between the + current and previous proof step. By default, the command shows the + output once with additions highlighted. Including “removed” shows + the output twice: once showing removals and once showing additions. + It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`. + .. cmdv:: Show Conjectures :name: Show Conjectures @@ -624,8 +630,11 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps and between -values in some error messages. +Coq can automatically highlight the differences between successive proof steps +and between values in some error messages. Also, as an experimental feature, +Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` +command, but only, for now, when using coqtop and Proof General. + For example, the following screenshots of CoqIDE and coqtop show the application of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. The conclusion is entirely in pale green because although it’s changed, no tokens were added @@ -795,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 75897fec45..853ddfd6dc 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1513,7 +1513,7 @@ In a goal like the following:: ============= m < 5 + n -The tactic ``abstract: abs n`` first generalizes the goal with respect ton +The tactic :g:`abstract: abs n` first generalizes the goal with respect to :g:`n` (that is not visible to the abstract constant abs) and then assigns abs. The resulting goal is:: @@ -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 ``````````````````````````````````` @@ -3756,8 +3756,11 @@ involves the following steps: the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals - are (quantified) equalities or double implications between a - term and an evar (e.g. ``m - m = ?F2 m`` in the running example). + are (quantified) Leibniz equalities, double implications or + registered relations (w.r.t. Class ``RewriteRelation``) between a + term and an evar, e.g. ``m - m = ?F2 m`` in the running example. + (This support for setoid-like relations is enabled as soon as we do + both ``Require Import ssreflect.`` and ``Require Setoid.``) 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. @@ -3769,7 +3772,10 @@ involves the following steps: by using a regular :tacn:`rewrite` tactic. 7. Interactive editing of the first n goals has to be signalled by - using the :tacn:`over` tactic or rewrite rule (see below). + using the :tacn:`over` tactic or rewrite rule (see below), which + requires that the underlying relation is reflexive. (The running + example deals with Leibniz equality, but ``PreOrder`` relations are + also supported, for example.) 8. Finally, a post-processing step is performed in the main goal to keep the name(s) for the bound variables chosen by the user in @@ -3795,6 +3801,10 @@ displayed as ``'Under[ … ]``): This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. +Note that a rewrite rule ``UnderE`` is available as well, if one wants +to "unprotect" the evar, without closing the goal automatically (e.g., +to instantiate it manually with another rule than reflexivity). + .. _under_one_liner: One-liner mode @@ -4061,6 +4071,7 @@ which the function is supplied: :name: congr This tactic: + + checks that the goal is a Leibniz equality; + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. @@ -4208,7 +4219,7 @@ in the second column. ``ident`` in all the occurrences of ``term2`` * - ``term1 as ident in term2`` - ``term 1`` - - in all the subterms identified by ``ident` + - in all the subterms identified by ``ident`` in all the occurrences of ``term2[term 1 /ident]`` The rewrite tactic supports two more patterns obtained prefixing the @@ -5013,7 +5024,7 @@ mechanism: Coercion is_true (b : bool) := b = true. This allows any boolean formula ``b`` to be used in a context where |Coq| -would expect a proposition, e.g., after ``Lemma … : ``. It is then +would expect a proposition, e.g., after ``Lemma … :``. It is then interpreted as ``(is_true b)``, i.e., the proposition ``b = true``. Coercions are elided by the pretty-printer, so they are essentially transparent to the user. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 78753fc053..53cfb973d4 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. @@ -555,12 +555,14 @@ Applying theorems This tactic applies to any goal. It behaves like :tacn:`exact` with a big difference: the user can leave some holes (denoted by ``_`` or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many - subgoals as there are holes in the term. The type of holes must be either - synthesized by the system or declared by an explicit cast + subgoals as there are remaining holes in the elaborated term. The type + of holes must be either synthesized by the system or declared by an explicit cast like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling - :tacn:`shelve_unifiable`. This low-level tactic can be - useful to advanced users. + :tacn:`shelve_unifiable`. The produced subgoals (shelved or not) + are *not* candidates for typeclass resolution, even if they have a type-class + type as conclusion, letting the user control when and how typeclass resolution + is launched on them. This low-level tactic can be useful to advanced users. .. example:: @@ -611,8 +613,9 @@ Applying theorems .. tacv:: simple notypeclasses refine @term :name: simple notypeclasses refine - This tactic behaves like :tacn:`simple refine` except it performs type checking - without resolution of typeclasses. + This tactic behaves like the combination of :tacn:`simple refine` and + :tacn:`notypeclasses refine`: it performs type checking without resolution of + typeclasses, does not perform beta reductions or shelve the subgoals. .. flag:: Debug Unification @@ -685,6 +688,28 @@ Applying theorems instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. + .. tacv:: rapply @term + :name: rapply + + The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it + uses the proof engine of :tacn:`refine` for dealing with + existential variables, holes, and conversion problems. This may + result in slightly different behavior regarding which conversion + problems are solvable. However, like :tacn:`apply` but unlike + :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes + which remain in :n:`@term` itself after typechecking and + typeclass resolution but before unification with the goal. More + technically, :n:`@term` is first parsed as a + :production:`constr` rather than as a :production:`uconstr` or + :production:`open_constr` before being applied to the goal. Note + that :tacn:`rapply` prefers to instantiate as many hypotheses of + :n:`@term` as possible. As a result, if it is possible to apply + :n:`@term` to arbitrarily many arguments without getting a type + error, :tacn:`rapply` will loop. + + Note that you need to :n:`Require Import Coq.Program.Tactics` to + make use of :tacn:`rapply`. + .. tacv:: simple apply @term. This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms @@ -804,11 +829,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 +1552,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 +2325,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 @@ -2824,11 +2849,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: cutrewrite <- (@term = @term’) :name: cutrewrite - This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`. + .. deprecated:: 8.5 + + This tactic can be replaced by :n:`enough (@term = @term’) as <-`. .. tacv:: cutrewrite -> (@term = @term’) - This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`. + .. deprecated:: 8.5 + + This tactic can be replaced by :n:`enough (@term = @term’) as ->`. .. tacn:: subst @ident @@ -2862,26 +2891,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 +3115,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 +3132,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 +3300,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 @@ -3281,11 +3310,13 @@ the conversion in hypotheses :n:`{+ @ident}`. defined transparent constant or local definition (see :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic - :tacn:`unfold` applies the :math:`\delta` rule to each occurrence of - the constant to which :n:`@qualid` refers in the current goal and - then replaces it with its :math:`\beta`:math:`\iota`-normal form. + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence + of the constant to which :n:`@qualid` refers in the current goal + and then replaces it with its :math:`\beta\iota\zeta`-normal form. + Use the general reduction tactics if you want to avoid this final + reduction, for instance :n:`cbv delta [@qualid]`. - .. exn:: @qualid does not denote an evaluable constant. + .. exn:: Cannot coerce @qualid to an evaluable reference. This error is frequent when trying to unfold something that has defined as an inductive type (or constructor) and not as a @@ -3548,7 +3579,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 +3607,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 +3751,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 +4227,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 @@ -4237,7 +4268,13 @@ some incompatibilities. .. tacv:: firstorder using {+ @qualid} - Adds lemmas :n:`{+ @qualid}` to the proof-search environment. If :n:`@qualid` + .. deprecated:: 8.3 + + Use the syntax below instead (with commas). + +.. tacv:: firstorder using {+, @qualid} + + Adds lemmas :n:`{+, @qualid}` to the proof-search environment. If :n:`@qualid` refers to an inductive type, it is the collection of its constructors which are added to the proof-search environment. @@ -4246,7 +4283,7 @@ some incompatibilities. Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search environment. -.. tacv:: firstorder @tactic using {+ @qualid} with {+ @ident} +.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident} This combines the effects of the different variants of :tacn:`firstorder`. @@ -4316,7 +4353,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 @@ -4887,6 +4924,8 @@ Performance-oriented tactic variants .. tacv:: convert_concl_no_check @term :name: convert_concl_no_check + .. deprecated:: 8.11 + Deprecated old name for :tacn:`change_no_check`. Does not support any of its variants. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 843459b723..89b24ea8a3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -195,7 +195,7 @@ Requests to the environment (see Section :ref:`invocation-of-tactics`). -.. cmd:: Eval @redexpr in @term +.. cmd:: Eval @red_expr in @term This command performs the specified reduction on :n:`@term`, and displays the resulting term with its type. The term to be reduced may depend on @@ -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) @@ -1146,7 +1146,7 @@ described first. Print all the currently non-transparent strategies. -.. cmd:: Declare Reduction @ident := @redexpr +.. cmd:: Declare Reduction @ident := @red_expr This command allows giving a short name to a reduction expression, for instance ``lazy beta delta [foo bar]``. This short name can then be used @@ -1158,7 +1158,7 @@ described first. functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but nothing prevents the user from also performing a - :n:`Ltac @ident := @redexpr`. + :n:`Ltac @ident := @red_expr`. .. seealso:: :ref:`performingcomputations` @@ -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 |