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

2 files changed, 15 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 98e6bad983..25b5ffc6ab 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,8 @@ Other tactics
 - In "simpl c" and "change c with d", c can be a pattern.
 - Tactic "revert" now preserves let-in's making it the exact inverse of
   "intro".
+- New tactics "clear dependent H" and "revert dependent H" that
+  clears (resp. reverts) H and all the hypotheses that depend on H.
 - Ltac's pattern-matching now supports matching metavariables that
   depend on variables bound upwards in the pattern.
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8fb0556545..07921978d5 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}}