Ajout ClearBody et Assert H:=t

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8260 85f007b7-540e-0410-9357-904b9bb8a0f7

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