Documentation of clear dependent and revert dependent

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

1 files changed, 13 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8fb055654..07921978d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -163,6 +163,11 @@ usable in the proof development.
   This tactic clears all hypotheses except the ones depending in 
   goal.
 
+\item {\tt clear dependent \ident \tacindex{clear dependent}}
+
+ This clears the hypothesis \ident\ and all hypotheses
+ which depend on it.
+
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -811,6 +816,14 @@ dependencies. This tactic is the inverse of {\tt intro}.
     used in the hypothesis} 
 \end{ErrMsgs}
 
+\begin{Variants}
+\item {\tt revert dependent \ident \tacindex{revert dependent}}
+
+ This moves to the goal the hypothesis \ident\ and all hypotheses
+ which depend on it.
+
+\end{Variants}
+
 \subsection{\tt change \term
 \tacindex{change}
 \label{change}}