Minor fix in doc for [unfold]

Close #9634

1 files changed, 6 insertions, 4 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 62d4aa704f..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