Fix #5413: [unfold ... in] not documented

Made a description of unfold...in and moved the index entry there.

1 files changed, 6 insertions, 1 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a2d45046b0..e06457fe46 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3523,8 +3523,13 @@ with its $\beta\iota$-normal form.
 \end{ErrMsgs}
 
 \begin{Variants}
+\item {\tt unfold {\qualid} in {\ident}}
+  \tacindex{unfold \dots in}
+
+  Replaces {\qualid} in hypothesis {\ident} with its definition
+  and replaces the hypothesis with its $\beta\iota$ normal form.
+
 \item {\tt unfold {\qualid}$_1$, \dots, \qualid$_n$}
-  \tacindex{unfold \dots\ in}
 
   Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$
   with their definitions and replaces the current goal with its