From c6ba56e2eac1a53be624901b3ac3b305efbef922 Mon Sep 17 00:00:00 2001
From: bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 9 Oct 2001 10:41:31 +0000
Subject: 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
---
 doc/RefMan-tac.tex | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc/RefMan-tac.tex')

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