diff options
Diffstat (limited to 'doc/sphinx/proof-engine/ltac.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 013ff0a83f..b1759bf71b 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1564,9 +1564,9 @@ Computing in a term: eval Evaluation of a term can be performed with: -.. tacn:: eval @red_expr in @term +:n:`eval @red_expr in @term` - :tacn:`eval` is a :token:`value_tactic`. +See :tacn:`eval`. :tacn:`eval` is a :token:`value_tactic`. Getting the type of a term ~~~~~~~~~~~~~~~~~~~~~~~~~~ |