From fcb04fbe8d6b82aa02d266db6d200b9fcb6ace04 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 20 May 2003 08:45:22 +0000
Subject: Ajout 'in (Type of ...)'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8334 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-tac.tex | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 9c553473c..b014ded70 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -806,6 +806,10 @@ Applies the conversion tactic {\convtactic} to the
 hypotheses \ident$_1$, \ldots, \ident$_n$. The tactic {\convtactic} is
 any of the conversion tactics listed in this section. 
 
+If $\ident$_i$ is a local definition, then $\ident$_i$ can be replaced
+by $(Type of \ident$_i)$ to adress not the body but the type of the
+local definition. Example: {\tt Unfold not in (Type of H1) (Type of H3).}
+
 \begin{ErrMsgs}
 \item \errindex{No such hypothesis} : {\ident}.
 \end{ErrMsgs}
@@ -2429,6 +2433,3 @@ user-defined tactics.
 %%% TeX-master: "Reference-Manual"
 %%% TeX-master: "Reference-Manual"
 %%% End: 
-
-
-
-- 
cgit v1.2.3