From c606dc386d81fc2f5e3aa6b3787f2095a0dee316 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 18 Jun 2010 17:14:20 +0000
Subject: 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
---
 doc/refman/RefMan-tac.tex | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'doc')

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}}
-- 
cgit v1.2.3