Ajout 'in (Type of ...)'

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

1 files changed, 4 insertions, 3 deletions

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: 
-
-
-