diff options
| author | filliatr | 2002-09-12 07:27:35 +0000 |
|---|---|---|
| committer | filliatr | 2002-09-12 07:27:35 +0000 |
| commit | 994931aa3290ad9d6e1ba12bc81198ba1c220550 (patch) | |
| tree | eb4f3cf839665661d1d077514e0bcee44865a99e | |
| parent | caa7751f2fcd80d1ddb4bb0dba5a578255b00bee (diff) | |
Subst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8291 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/RefMan-tac.tex | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 34aa2a2254..e345d1b09f 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -1186,6 +1186,22 @@ This tactic applies to a goal which have form {\tt t=u} and transforms it into the two subgoals {\tt t={\term}} and {\tt {\term}=u}. +\subsection{\tt Subst {\ident}}\tacindex{Subst} +This tactic applies to a goal which have \ident\ in its context and +(at least) one hypothesis, say {\tt H}, of type {\tt + \ident=t}. Then it replaces +\ident\ by {\tt t} everywhere in the goal (in the hypotheses +and in the conclusion) and clears \ident\ and {\tt H} from the context. + +\Rem +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$} +\end{Variants} + + \section{Equality and inductive sets} We describe in this section some special purpose tactics dealing with equality and inductive sets or |