MAJ du manuel de référence (modules+fixpoints+pose proof)

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

1 files changed, 9 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index aaa2ee51f4..ae3d8fe043 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -535,6 +535,11 @@ in the list of subgoals remaining to prove.
 
    This tactic behaves like \texttt{assert ({\ident} : {\form})}.
 
+\item \texttt{pose proof {\term} as {\ident}}
+
+  This tactic behaves like \texttt{assert ({\ident:T} by exact {\term}} where
+  \texttt{T} is the type of {\term}. 
+
 \end{Variants}
 
 % PAS CLAIR;
@@ -1275,6 +1280,10 @@ last introduced hypothesis.
 {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
 {\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}.
 
+\item \texttt{pose proof {\term} as {\intropattern}}
+
+  This tactic behaves like \texttt{destruct {\term} as {\intropattern}}.
+
 \item{\tt destruct {\term} using {\qualid}}
 
   This is a synonym of {\tt induction {\term} using {\qualid}}.