diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-16 08:40:07 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-09-16 08:40:07 +0000 |
| commit | 347d8c7e6baa58a44ab6f988060b416b4936316e (patch) | |
| tree | f06c0c2a9badf00ce1c63b28e27aaa68478b16a5 /doc | |
| parent | 994931aa3290ad9d6e1ba12bc81198ba1c220550 (diff) | |
documentation variante Subst (sans argument)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8292 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -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 e345d1b09..6358bc1c8 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} |