diff options
Diffstat (limited to 'doc/sphinx/proof-engine/ltac.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 6 |
1 files changed, 3 insertions, 3 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`. |