diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index a2d45046b..e06457fe4 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 |