diff options
| -rw-r--r-- | doc/RefMan-tac.tex | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 28307b4f35..d5da2e3202 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -197,6 +197,17 @@ then all hypotheses between {\ident$_1$} and {\ident$_2$} which it depends on {\ident$_2$}} \end{ErrMsgs} +\subsection{\tt Rename {\ident$_1$} into {\ident$_2$}.}\tacindex{Rename} +This renames hypothesis {\ident$_1$} into {\ident$_2$} in the current +context\footnote{but it does not rename the hypothesis in the +proof-term...} + +\begin{ErrMsgs} +\item \errindex{No such assumption} + +\item \errindex{{\ident$_2$} is already used} +\end{ErrMsgs} + \subsection{\tt Intro} \tacindex{Intro} \label{Intro} @@ -404,6 +415,16 @@ which should not be substituted. This is the general form. It substitutes {\term} at occurrences {\num$_1^i$} \dots\ {\num$_{n_i}^i$} of hypothesis {\ident$_i$}. One of the {\ident}'s may be the word {\tt Goal}. + +\item{\tt Pose {\ident} := {\term}}\tacindex{Pose}\\ + This adds the local definition {\ident} := {\term} to the current + context without performing any replacement in the goal or in the + hypotheses. + +\item{\tt Pose {\term}}\\ + This behaves as {\tt Pose {\ident} := {\term}} but {\ident} is + generated by {\Coq}. + \end{Variants} \subsection{\tt Assert {\ident} : {\form}}\tacindex{Assert} |