documentation of f_equal and revert and case_eq (and s/lri.fr/pps.jussieu.fr/ in my bib entry)

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

1 files changed, 30 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2caf3b109..5a0a6238d 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -665,6 +665,10 @@ to $T$.
   This generalizes {\term} but also {\em all} hypotheses which depend
   on {\term}. It clears the generalized hypotheses.
 
+\item {\tt revert \term$_1$ \dots\ \term$_n$}\tacindex{revert}
+ 
+  This is equivalent to a {\tt generalize} followed by a {\tt clear}.
+
 \end{Variants}
 
 \subsection{\tt change \term
@@ -1396,6 +1400,15 @@ last introduced hypothesis.
   analysis without recursion. It behaves as {\tt elim \term} but using
   a case-analysis elimination principle and not a recursive one.
 
+\item{\tt case\_eq \term}\label{case_eq}\tacindex{case\_eq}
+
+ The tactic {\tt case\_eq} is a variant of the {\tt case} tactic that
+ allow to perform case analysis on a term without completely 
+ forgetting its original form. This is done by generating 
+ equalities between the original form of the term and the outcomes of 
+ the case analysis. 
+
+
 \item {\tt case {\term} with \term$_1$ \dots\ \term$_n$}
   \tacindex{case \dots\ with}
 
@@ -1414,6 +1427,7 @@ last introduced hypothesis.
   {\tt intros until {\num}} to the {\num}-th non-dependent premise of
   the goal.
 
+
 \end{Variants}
 
 \subsection{\tt intros {\intropattern} {\ldots} {\intropattern}
@@ -1827,6 +1841,22 @@ and are registered using the command
 \end{quote}
 \end{Variants}
 
+
+\subsection{\tt f\_equal
+\label{f-equal}
+\tacindex{f\_equal}}
+
+This tactic applies to a goal of the form $f\ a_1\ \ldots\ a_n = f'\
+a'_1\ \ldots\ a'_n$. Using {\tt f\_equal} on such a goal leads to
+subgoals $f=f'$ and $a_1=a'_1$ and so on up to $a_n=a'_n$. Amongst 
+these subgoals, the simple ones (e.g. provable by
+reflexivity or congruence) are automatically solved by {\tt f\_equal}.
+
+\Rem {\tt f\_equal} currently handles goals with only up to 5 arguments
+(i.e. $n\leq 5$). 
+
+
+
 \section{Equality and inductive sets}
 
 We describe in this section some special purpose tactics dealing with