From 461538c2fb88234c46081bc4749814ec202eaadd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 21 Nov 2019 21:11:47 +0100
Subject: Minor fix in doc for [unfold]

Close #9634
---
 doc/sphinx/proof-engine/tactics.rst | 10 ++++++----
 1 file 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
-- 
cgit v1.2.3