Adding documentation for a variant of Inversion, where a numeric argument,

referring to the nth non-dependent product in the goal's conclusion, can be given
instead of an hypothesis name.


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

1 files changed, 4 insertions, 0 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 1275134af..33238d7f6 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1337,6 +1337,10 @@ conditions that should hold for the instance $(I~\vec{t})$ to be
 proved by $c_i$.
 
 \begin{Variants}
+\item \texttt{Inversion} \num\\
+  This does the same thing as \texttt{Intros until \num} then
+\texttt{Inversion \ident} where \ident is the identifier for the last
+introduced hypothesis.
 \item \texttt{Inversion\_clear} \ident\\
   \tacindex{Inversion\_clear}
   That does \texttt{Inversion} and then erases \ident~ from the