diff options
| -rw-r--r-- | doc/RefMan-tac.tex | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 39b552835f..afefa32046 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -161,8 +161,19 @@ This tactic erases the hypothesis named {\ident} in the local context of the current goal. Then {\ident} is no more displayed and no more usable in the proof development. +\begin{Variants} +\item {\tt Clear {\ident$_1$} \ldots {\ident$_n$}.}\\ +This is equivalent to {\tt Clear {\ident$_1$}. \ldots Clear {\ident$_n$}.} + +\item {\tt ClearBody {\ident}.}\tacindex{ClearBody}\\ +This tactic expects {\ident} to be a local definition then clears its +body. Otherwise said, this tactic turns a definition into an assumption. +\end{Variants} + \begin{ErrMsgs} \item \errindex{No such assumption} +\item \errindex{{\ident} is used in the conclusion} +\item \errindex{{\ident} is used in the hypothesis {\ident'}} \end{ErrMsgs} \subsection{\tt Move {\ident$_1$} after {\ident$_2$}.}\tacindex{Move} @@ -412,6 +423,10 @@ subgoals remaining to prove. This behaves as {\tt Assert {\ident} : {\form}} but {\ident} is generated by {\Coq}. +\item{\tt Assert {\ident} := {\term}}\\ + This behaves as {\tt Assert {\ident} : {\type};[Exact +{\term}|Idtac]} where {\type} is the type of {\term}. + \item {\tt Cut {\form}}\tacindex{Cut} \\ This tactic applies to any goal. It implements the non dependent case of the ``App''\index{Typing rules!App} rule given in section |