Include can accept both Module and Module Type

 Syntax Include Type is still active, but deprecated, and triggers a warning.
 The syntax M <+ M' <+ M'', which performs internally an Include, also
 benefits from this: M, M', M'' can be independantly modules or module type.

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

1 files changed, 11 insertions, 27 deletions

diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 4d213e1f2d..40fd6f1102 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -65,23 +65,17 @@ This command is used to start an interactive module named {\ident}.
 \subsubsection{Reserved commands inside an interactive module:
 \comindex{Include}}
 \begin{enumerate}
-\item {\tt Include {\modexpr}}
+\item {\tt Include {\module}}
 
- Includes the content of {\modexpr} in the current interactive module type. If {\modexpr} is a high-order module expression then the system tries to instanciate {\modexpr}
+  Includes the content of {\module} in the current interactive
+ module. Here {\module} can be a module expresssion or a module type
+ expression. If {\module} is a high-order module or module type
+ expression then the system tries to instanciate {\module}
  by the current interactive module.
 
-\item {\tt Include Type {\modtype}}
+\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
 
- Includes the content of {\modtype} in the current interactive module type. If  {\modtype} is a high-order module type expression then the system tries to instanciate {\modtype}
- by the current interactive module.
-
-\item {\tt Include {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}} 
-
-is a shortcut for {\tt Include {\modexpr$_1$}}  $\ldots$ {\tt Include {\modexpr$_n$}}
-
-\item {\tt Include Type {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}} 
-
-is a shortcut for {\tt Include Type {\modtype$_1$}}  $\ldots$ {\tt Include Type {\modtype$_n$}}
+is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
 \end{enumerate}
 \subsection{\tt End {\ident}
 \comindex{End}}
@@ -151,23 +145,13 @@ This command is used to start an interactive module type {\ident}.
 \subsubsection{Reserved commands inside an interactive module type:
 \comindex{Include}\comindex{Inline}}
 \begin{enumerate}
-\item {\tt Include {\modexpr}}
-
- Includes the content of {\modexpr} in the current interactive module type. If {\modexpr} is a high-order module expression then the system tries to instanciate {\modexpr}
- by the current interactive module type.
-
-\item {\tt Include Type {\modtype}}
-
- Includes the content of {\modtype} in the current interactive module type. If {\modtype} is a high-order module type expression then the system tries to instanciate {\modtype}
- by the current interactive module type.
-
-\item {\tt Include {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}} 
+\item {\tt Include {\module}}
 
-is a shortcut for {\tt Include {\modexpr$_1$}}  $\ldots$ {\tt Include {\modexpr$_n$}}
+ Same as {\tt Include} inside a module.
 
-\item {\tt Include Type {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}} 
+\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
 
-is a shortcut for {\tt Include Type {\modtype$_1$}}  $\ldots$ {\tt Include Type {\modtype$_n$}}
+is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
 
 \item {\tt {\declarationkeyword} Inline {\assums} }