From b57475e03b5d00b98829162ef6183b6c2655807c Mon Sep 17 00:00:00 2001
From: Johannes Kloos
Date: Tue, 24 Oct 2017 01:07:18 +0200
Subject: Fix #5413: [unfold ... in] not documented

Made a description of unfold...in and moved the index entry there.
---
 doc/refman/RefMan-tac.tex | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3