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

3 files changed, 27 insertions, 32 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index a851a334c..6cc6dd5c7 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1231,8 +1231,8 @@ argument. They are needed to ensure that the {\tt Fixpoint} definition
 always terminates. The point of the {\tt \{struct \ident {\tt \}}}
 annotation is to let the user tell the system which argument decreases
 along the recursive calls. This annotation may be left implicit for
-fixpoints with one argument. For instance, one can define the addition
-function as :
+fixpoints where only one argument has an inductive type. For instance,
+one can define the addition function as :
 
 \begin{coq_example}
 Fixpoint add (n m:nat) {struct n} : nat :=
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 9f6f2abce..44a88034f 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -55,6 +55,11 @@ This command is used to start an interactive module named {\ident}.
   {\modbindings}. The output module type is verified against the
   module type {\modtype}.
 
+\item\texttt{Module [Import|Export]}
+
+  Behaves like \texttt{Module}, but automatically imports or exports
+  the module.
+
 \end{Variants}
 
 \subsection{\tt End {\ident}
@@ -139,38 +144,9 @@ Defines a module type {\ident} equal to {\modtype}.
   {\modbindings} and returning {\modtype}.
 \end{Variants}
 
-\subsection{\tt Declare Module {\ident}}
-
-Starts an interactive module declaration. This command is available
-only in module types. 
-
-\begin{Variants}
-
-\item{\tt Declare Module {\ident} {\modbindings}}
-
-  Starts an interactive declaration of a functor with parameters given
-  by {\modbindings}.
-
-% Particular case of the next item
-%\item{\tt Declare Module {\ident} \verb.<:. {\modtype}}
-%
-%  Starts an interactive declaration of a module satisfying {\modtype}.
-
-\item{\tt Declare Module {\ident} {\modbindings} \verb.<:. {\modtype}}
-
-  Starts an interactive declaration of a functor with parameters given
-  by {\modbindings} (possibly none). The declared output module type is
-  verified against the module type {\modtype}.
-
-\end{Variants}
-
-\subsection{\tt End {\ident}}
-
-This command closes the interactive declaration of module {\ident}.
-
 \subsection{\tt Declare Module {\ident} : {\modtype}}
 
-Declares a module of {\ident} of type {\modtype}. This command is available
+Declares a module {\ident} of type {\modtype}. This command is available
 only in module types. 
 
 \begin{Variants}
@@ -189,6 +165,11 @@ only in module types.
   Declares a module equal to the module {\qualid}, verifying that the
   module type of the latter is a subtype of {\modtype}.
 
+\item\texttt{Declare Module [Import|Export] {\ident} := {\qualid}}
+
+  Declares a modules {\ident} of type {\modtype}, and imports or
+  exports it directly.
+
 \end{Variants}
 
 
@@ -389,6 +370,11 @@ Prints the module type and (optionally) the body of the module {\ident}.
 
 Prints the module type corresponding to {\ident}.
 
+\subsection{\texttt{Locate Module {\qualid}}
+\comindex{Locate Module}}
+
+Prints the full name of the module {\qualid}.
+
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index aaa2ee51f..ae3d8fe04 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}}.