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

2 files changed, 20 insertions, 8 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 9d88fa077e..defcb45965 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -203,10 +203,14 @@ obligations (e.g. when defining mutually recursive blocks). The optional
 tactic is replaced by the default one if not specified.
 
 \begin{itemize}
-\item {\tt Obligation Tactic := \tacexpr}\comindex{Obligation Tactic}
+\item {\tt [Local|Global] Obligation Tactic := \tacexpr}\comindex{Obligation Tactic}
   Sets the default obligation
   solving tactic applied to all obligations automatically, whether to
   solve them or when starting to prove one, e.g. using {\tt Next}.
+  Local makes the setting last only for the current module. Inside
+  sections, local is the default.
+\item {\tt Show Obligation Tactic}\comindex{Show Obligation Tactic}
+  Displays the current default tactic.
 \item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining
   obligations.
 \item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of
@@ -270,5 +274,5 @@ Program Fixpoint f (x : A | P) { measure size } :=
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
+%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage2 doc/refman/Reference-Manual.pdf"
 %%% End: 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4d5cdbb81c..ab8cfd07af 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}}