diff options
| -rw-r--r-- | doc/RefMan-tac.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index e345d1b09f..6358bc1c8f 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -1198,7 +1198,10 @@ When several hypotheses have the form {\tt \ident=t}, the first one is used. \begin{Variants} \item {\tt Subst \ident$_1$ \dots \ident$_n$} \\ - Is equivalent to {\tt Subst \ident$_1$; \dots; Subst \ident$_n$} + Is equivalent to {\tt Subst \ident$_1$; \dots; Subst \ident$_n$}. + \item {\tt Subst} \\ + Applies {\tt Subst} repeatedly to all identifiers from the context + for which an equality exists. \end{Variants} |