Update CHANGES, add documentation for new commands/tactics and do a bit

of cleanup in tactics/


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

1 files changed, 14 insertions, 6 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4d5cdbb81..ab8cfd07a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -795,14 +795,22 @@ where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by
   This generalizes {\term} but also {\em all} hypotheses which depend
   on {\term}. It clears the generalized hypotheses.
 
-\item {\tt revert \ident$_1$ \dots\ \ident$_n$}\tacindex{revert}
- 
-  This is equivalent to a {\tt generalize} followed by a {\tt clear}
-  on the given hypotheses. This tactic can be seen as reciprocal to 
-  {\tt intros}. 
-
 \end{Variants}
 
+
+\subsection{\tt revert  \ident$_1$ \dots\ \ident$_n$
+\tacindex{revert}
+\label{revert}}
+
+This applies to any goal with variables \ident$_1$ \dots\ \ident$_n$.
+It moves the hypotheses (possibly defined) to the goal, if this respects
+dependencies. This tactic is the inverse of {\tt intro}. 
+
+\begin{ErrMsgs}
+\item \errindexbis{{\ident} is used in the hypothesis {\ident'}}{is
+    used in the hypothesis} 
+\end{ErrMsgs}
+
 \subsection{\tt change \term
 \tacindex{change}
 \label{change}}