diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 20 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 6 |
3 files changed, 20 insertions, 12 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index e37f300915..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` @@ -986,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`. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ad7f9af0f9..4f903d5776 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3281,11 +3281,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 @@ -4237,7 +4239,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 +4254,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`. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e87b76b4ab..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 @@ -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` |