Doc module, premiere version

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

6 files changed, 796 insertions, 13 deletions

diff --git a/doc/Makefile b/doc/Makefile
index e66171180d..187c48e4aa 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -13,7 +13,7 @@
 #   - htmlSplit: http://coq.inria.fr/~delahaye
 # Rapports INRIA: dviselect, rrkit (par Michel Mauny)
 
-DOCCOQTOP=$(COQBIN)/coqtop.byte
+DOCCOQTOP=$(COQBIN)/coqtop #.byte
 DOCCOQC=$(COQBIN)/coqc
 COQTEX=$(COQBIN)/coq-tex -image $(DOCCOQTOP) -v -sl -small
 #COQWEBSTY=$(HOME)/lib/tex/
@@ -35,7 +35,7 @@ LIBFILES=library/Logic.tex library/Datatypes.tex library/Peano.tex \
          library/Wf.tex library/Specif.tex
 
 REFMANCOQTEXFILES=\
-  RefMan-gal.v.tex RefMan-ext.v.tex RefMan-tac.v.tex \
+  RefMan-gal.v.tex RefMan-ext.v.tex RefMan-mod.v.tex RefMan-tac.v.tex \
   RefMan-cic.v.tex RefMan-lib.v.tex RefMan-tacex.v.tex \
   RefMan-syn.v.tex RefMan-ltac.v.tex RefMan-oth.v.tex
 
@@ -45,6 +45,7 @@ COQTEXFILES= Cases.v.tex Coercion.v.tex Extraction.v.tex Program.v.tex\
 
 REFMANFILES= Reference-Manual.tex RefMan-pre.tex RefMan-int.tex \
   RefMan-pro.tex RefMan-com.tex RefMan-uti.tex RefMan-add.tex \
+  RefMan-modr.tex \
   $(REFMANCOQTEXFILES) 
 
 REFMAN=Reference-Manual
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 64bae0c436..84f0a09ebf 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -126,7 +126,7 @@ Qed.
 \end{coq_example*}
 \begin{coq_example}
 Definition half := (mkRat true (1) (2) (O_S (1)) one_two_irred).
-\end{coq_example*}
+\end{coq_example}
 \begin{coq_example}
 Check half.
 \end{coq_example}
@@ -200,7 +200,7 @@ empty.
 \begin{figure}[t]
 \begin{tabular}{|rcl|}
 \hline
-{\nestedpattern}  & := & {\ident} \\
+{\nestedpattern}  & ::= & {\ident} \\
  & $|$ & \_ \\
  & $|$ & \texttt{(} {\ident} \nelist{\nestedpattern}{} \texttt{)} \\
  & $|$ & \texttt{(} {\nestedpattern} \texttt{as}  {\ident} \texttt{)} \\
@@ -208,13 +208,13 @@ empty.
  & $|$ & \texttt{(} {\nestedpattern} \texttt{)} \\
  &&\\
 
-{\multpattern} & := &  \nelist{nested\_pattern}{} \\
+{\multpattern} & ::= &  \nelist{nested\_pattern}{} \\
  && \\
 
-{\exteqn} & := &  {\multpattern} \texttt{=>} {\term} \\
+{\exteqn} & ::= &  {\multpattern} \texttt{=>} {\term} \\
  && \\
 
-{\term} & := &  
+{\term} & ::= &  
  \zeroone{\annotation} \texttt{Cases} \nelist{\term}{} \texttt{of} 
 \sequence{\exteqn}{$|$} \texttt{end} \\
 \hline
@@ -234,7 +234,7 @@ constructors without arguments), it is possible to use a {\tt if
 
 \medskip
 \begin{tabular}{rcl}
-term & := & \zeroone{\annotation} {\tt if} {\term} {\tt then} {\term} {\tt else} {\term}\\
+term & ::= & \zeroone{\annotation} {\tt if} {\term} {\tt then} {\term} {\tt else} {\term}\\
 \end{tabular}
 \medskip
 
@@ -501,8 +501,7 @@ Note the difference between the value of {\tt x'} inside section {\tt
   s1} and outside.
 
 \begin{ErrMsgs}
-\item \errindex{Section {\ident} does not exist (or is already closed)}
-\item \errindex{Section {\ident} is not the innermost section}
+\item \errindex{This is not the last opened section}
 \end{ErrMsgs}
 
 \begin{Remarks}
@@ -519,6 +518,8 @@ section is closed.
 %module with an identifier already used in the module (see \ref{compiled}).
 \end{Remarks}
 
+\input{RefMan-mod.v}
+
 \section{Logical paths of libraries and compilation units}
 \label{Libraries}
 \index{Libraries}
diff --git a/doc/RefMan-mod.tex b/doc/RefMan-mod.tex
new file mode 100644
index 0000000000..cb6b32b9f1
--- /dev/null
+++ b/doc/RefMan-mod.tex
@@ -0,0 +1,206 @@
+\section{Module system}
+
+The module system provides a way of packaging related elements
+together, as well as a mean of massive abstraction.
+
+\begin{figure}[t]
+\begin{tabular}{|rcl|}
+\hline
+{\modtype}  & ::= & {\ident} \\
+ & $|$ & \modtype \texttt{ with Definition }{\ident} \verb.:=. {\term} \\
+ & $|$ & \modtype \texttt{ with Module }{\ident} \verb.:=. {\qualid} \\
+ &&\\
+
+{\onemodbinding}  & ::= & \nelist{\ident}{\texttt{,}} \verb.:. {\modtype} \\
+ &&\\
+
+{\modbindings} & ::= & \nelist{\onemodbinding}{\texttt{;}}\\
+ &&\\
+
+{\modexpr} & ::= & \nelist{\qualid}{} \\
+\hline
+\end{tabular}
+\caption{Syntax of modules.}
+\label{ecases-grammar}
+\end{figure}
+
+\subsection{\tt Module {\ident}}\comindex{Module}
+This command is used to start an interactif module named {\ident}.
+
+\begin{Variants}
+\item{\tt Module \ident [\modbindings]}\\
+  Starts an interactif functor with parameters given by {\modbindings}.
+\item{\tt Module {\ident} \verb.:. \modtype}\\
+  Starts an interactif module specifying its the module type. 
+\item{\tt Module {\ident} [\modbindings] \verb.:. \modtype}\\
+  Starts an interactif functor with parameters given by
+  {\modbindings}, and output module type \modtype.
+\end{Variants}
+
+\subsection{\tt End {\ident}}\comindex{End}
+This command closes the interactif module {\ident}. If the module type
+was given the content of the module is matched against it and an error
+is signaled if the matching fails. If the module is basic (is not a
+functor) ist components (constants, inductives, submodules etc) are
+now available through the dot notation.
+
+\begin{ErrMsgs}
+\item \errindex{No such label {\ident}}
+\item \errindex{Signature components for label {\ident} do not match}
+\item \errindex{This is not the last opened module}
+\end{ErrMsgs}
+
+
+\subsection{\tt Module {\ident} := {\modexpr}}\comindex{Module}
+This command defines the module identifier {\ident} to be equal to \modexpr.
+
+\begin{Variants}
+\item{\tt Module \ident [\modbindings] := {\modexpr}}\\
+  Defines a functor with parameters given by {\modbindings} and body \modexpr.
+\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}}\\
+  Defines a module specifying its module type.
+\item{\tt Module {\ident} [\modbindings] \verb.:. {\modtype} := {\modexpr}}\\
+  Defines a functor with parameters given by {\modbindings}, and
+  output module type \modtype, with body {\modexpr}.
+\end{Variants}
+
+\subsection{\tt Module Type {\ident}}\comindex{Module Type}
+This command is used to start an interactif module type {\ident}.
+
+\begin{Variants}
+\item{\tt Module \ident [\modbindings]}\\
+  Starts an interactif functor type with parameters given by {\modbindings}.
+\end{Variants}
+
+\subsection{\tt End {\ident}}\comindex{End}
+This command closes the interactif module type {\ident}.
+
+\begin{ErrMsgs}
+\item \errindex{This is not the last opened module type}
+\end{ErrMsgs}
+
+\subsection{\tt Module Type {\ident} := {\modtype}}
+Define a module type \ident equal to \modtype.
+
+\begin{Variants}
+\item {\tt Module Type {\ident} {\modbindings} := {\modtype}} \\
+  Define a functor type {\ident} specifying functors taking arguments
+  {\modbindings} and returning {\modtype}.
+\end{Variants}
+
+\subsubsection{Example}
+
+Let us define a simple module.
+\begin{coq_example}
+Module M.
+  Definition T:=nat.
+  Definition x:=O.
+  Definition y:bool.
+    Exact true.
+  Defined.
+End M.
+\end{coq_example}
+Inside a module one can define constants, prove thorems and do any
+other things that can be done in the toplevel. Components of a closed
+module can be accessed using the dot notation:
+\begin{coq_example}
+Print M.x.
+\end{coq_example}
+A simple module type:
+\begin{coq_example}
+Module Type SIG.
+  Definition T:Set.
+  Definition x:T.
+End SIG.
+\end{coq_example}
+Notice that \texttt{Definition}\ without body did not start the proof
+mode. Also \texttt{Lemma} or \texttt{Theorem} do not start one.
+Inside a module type \texttt{Definition}\ withount body,
+\texttt{Lemma}, \texttt{Theorem}, \texttt{Axiom}, \texttt{Parameter} are
+equivalent.
+
+Now we can create a new module from \texttt{M}, giving it a less
+precise specification: the \texttt{y} component is dropped as well
+as the body of \texttt{x}.
+\begin{coq_example}
+Module N  :  SIG with Definition T:=nat  :=  M.
+Print N.T.
+Print N.x.
+Print N.y.
+\end{coq_example}
+\begin{coq_eval}
+Reset N.
+\end{coq_eval}
+The definition of \texttt{N} using the module type expression
+\texttt{SIG with Definition T:=nat} is equivalent to the following
+one:
+\begin{coq_example*}
+Module Type SIG'.
+  Definition T:Set:=nat.
+  Definition x:T.
+End SIG'.
+Module N : SIG' := M.
+\end{coq_example*}
+Now let us create a functor
+\begin{coq_example}
+Module Two[X,Y:SIG].
+\end{coq_example}
+\begin{coq_example*}
+  Definition T:=X.T * Y.T.
+  Definition x:=(X.x, Y.x).
+\end{coq_example*}
+\begin{coq_example}
+End Two.
+\end{coq_example}
+and apply it to our modules and do some computations
+\begin{coq_example}
+Module P:=Two M N.
+Eval Compute in (plus (Fst P.x) (Snd P.x)).
+\end{coq_example}
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{Remarks}
+\item Modules and module types can be nested components of each other.
+\item When a module is started inside a module type,
+  \texttt{Definition} without body, \texttt{Lemma}, and
+  \texttt{Theorem} still do not start the proof mode.  This is still a
+  specification (of a sub-module component) and not a real definition.
+\item The only way of using a proof mode in a module type is using the 
+  \texttt{Goal} command.
+\item One can have sections inside a module or a module type, but
+  not a module or a module type inside a section.
+\item Other commands like \texttt{Hint} or \texttt{Syntactic
+    Definition} can also appear inside modules and module types. In
+    case of a module definition like:
+
+    \medskip
+    \noindent
+    {\tt Module N : SIG := M.} 
+    \medskip
+
+    or
+
+    \medskip
+    {\tt Module N : SIG.\\
+      \ \ \dots\\
+      End N.}
+    \medskip 
+
+    the commands valid for \texttt{N} are not those from
+    \texttt{M} (or the module body) but the ones from \texttt{SIG}.
+
+\end{Remarks}
+
+\subsection{\tt Print Module {\ident}}\comindex{Print Module}
+Prints the module type and the body of the module {\ident}.
+
+\subsection{\tt Print Module Type {\ident}}\comindex{Print Module Type}
+Prints the module type correspondint to {\ident}.
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex
new file mode 100644
index 0000000000..034c6a3952
--- /dev/null
+++ b/doc/RefMan-modr.tex
@@ -0,0 +1,545 @@
+\chapter{The Module System}
+\label{Mod}
+
+The module system extends the Calculus of Inductive Constructions
+providing a convinient way to structure large developments as well as
+a mean of massive abstraction.
+
+\section{Modules and module types}
+
+\paragraph{Access path.} It is denoted by $p$, it can be either a module 
+variable $X$ or, if $p'$ is an access path and $id$ an identifier, then
+$p'.id$ is an access path.
+
+\paragraph{Structure element.} It is denoted by \Impl\ and is either a
+definition of a constant, an assumption, a definition of an inductive
+or a definition of a module or a module type abbreviation.
+
+\paragraph{Module expression.} It is denoted by $M$ and can be:
+\begin{itemize}
+\item an access path $p$
+\item a structure $\struct{\nelist{\Impl}{;}}$
+\item a functor $\functor{X}{T}{M'}$, where $X$ is a module variable,
+  $T$ is a module type and $M'$ is a module expression
+\item an application of access paths $p' p''$
+\end{itemize}
+
+\paragraph{Signature element.} It is denoted by \Spec, it is a
+specification of a constant, an assumption, an inducitive, a module or
+a module type abbreviation.
+
+\paragraph{Module type}, denoted by $T$ can be:
+\begin{itemize}
+\item a module type name
+\item an access path $p$
+\item a signature $\sig{\nelist{\Spec}{;}}$
+\item a functor type $\funsig{X}{T'}{T''}$, where $T'$ and $T''$ are
+  module types
+\end{itemize}
+
+\paragraph{Module definition}, written $\Mod{X}{T}{M}$ can be a
+structure element. It consists of a module variable $X$, a module type
+$T$ and a module expression $M$.
+
+\paragraph{Module specification}, written $\ModS{X}{T}$ or
+$\ModSEq{X}{T}{p}$ can be a signature element or a part of an
+environment. It consists of a module variable $X$, a module type $T$
+and, optionally, a module path $p$. 
+
+\paragraph{Module type abbreviation}, written $\ModType{S}{T}$, where
+$S$ is a module type name and $T$ is a module type.
+
+
+\section{Typing Modules}
+
+In order to introduce the typing system we must first slightly extend
+the syntactic class of terms and environments given in
+section~\ref{Terms}. The environments, apart from definitions of
+constants and inductives will also hold any other signature elements.
+Terms, apart from variables, constants and complex terms, will also
+include access paths.
+
+We will also need additional typing judgments: 
+\begin{itemize}
+\item \WFT{E}{T}, denoting that a module type $T$ is well-formed, 
+
+\item \WTM{E}{M}{T}, denoting that a module expression $M$ has type $T$ in
+environment $E$.
+
+\item \WTM{E}{\Impl}{\Spec}, denoting that an implementation $\Impl$
+  verifies a specification $\Spec$
+
+\item \WS{E}{T_1}{T_2}, denoting that a module type $T_1$ is a subtype of a
+module type $T_2$.
+
+\item \WS{E}{\Spec_1}{\Spec_2}, denoting that a specification
+  $\Spec_1$ is more precise that a specification $\Spec_2$.
+\end{itemize}
+The rules for forming module types are the following:
+\begin{itemize}
+\item [WF-SIG]
+\inference{%
+  \frac{
+    \WF{E;E'}{}
+  }{%%%%%%%%%%%%%%%%%%%%%
+    \WFT{E}{\sig{E'}}
+  }
+}
+\item [WF-FUN]
+\inference{%
+  \frac{
+    \WFT{E;\ModS{X}{T}}{T'}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WFT{E}{\funsig{X}{T}{T'}}
+  }
+}
+\end{itemize}
+Rules for typing module expressions:
+\begin{itemize}
+\item [MT-STRUCT]
+\inference{%
+  \frac{
+    \begin{array}{c}
+      \WFT{E}{\sig{\Spec_1;\dots;\Spec_n}}\\
+      \WTM{E;\Spec_1;\dots;\Spec_{i-1}}{\Impl_i}{\Spec_i}
+                                              \textrm{ \ \ for } i=1\dots n
+    \end{array}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WTM{E}{\struct{\Impl_1;\dots;\Impl_n}}{\sig{\Spec_1;\dots;\Spec_n}}
+  }
+}
+\item [MT-FUN]
+\inference{%
+  \frac{
+    \WTM{E;\ModS{X}{T}}{M}{T'}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WTM{E}{\functor{X}{T}{M}}{\funsig{X}{T}{T'}}
+  }
+}
+\item [MT-APP]
+\inference{%
+  \frac{
+    \WTM{E}{p'}{\funsig{X}{T}{T'}}~~~~~~~~~~~\WTM{E}{p''}{T}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WTM{E}{p' p''}{T'\{X/p''\}}
+  }
+}
+\item [MT-SUB]
+\inference{%
+  \frac{
+    \WTM{E}{M}{T}~~~~~~~~~~~~\WS{E}{T}{T'}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WTM{E}{M}{T'}
+  }
+}
+\item [MT-STR]
+\inference{%
+  \frac{
+    \WTM{E}{p}{T}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WTM{E}{p}{T/p}
+  }
+}
+\end{itemize}
+The last rule, called strengthenning is used to make all module fields
+manifestly equal to themselves. The notation $T/p$ has the following
+meaning:
+\begin{itemize}
+\item if $T=\sig{\Spec_1;\dots;\Spec_n}$ then
+  $T/p=\sig{\Spec_1/p;\dots;\Spec_n/p}$ where $\Spec/p$ is defined as
+  follows:
+  \begin{itemize}
+  \item $\Def{}{c}{U}{t}/p ~=~ \Def{}{c}{U}{t}$
+  \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{U}{p.c}$
+  \item $\ModS{X}{T}/p ~=~ \ModSEq{X}{T/p.X}{p.X}$
+  \item $\ModSEq{X}{T}{p'}/p ~=~ \ModSEq{X}{T}{p'}$
+  \item $\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$
+  \item $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}$
+  \end{itemize}
+\item if $T=\funsig{X}{T}{T'}$ then $T/p=T$
+\item if $T$ is an access path or a module type name, then we have to
+  unfold its definition and proceed according to the rules above. 
+\end{itemize}
+The notation $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ denotes an
+inductive definition that is definitionally equal to the inductive
+definition in the module denoted by the path $p$. All rules which have
+$\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}$ as premises are also valid for 
+$\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$. We give the formation rule
+for $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ below as well as
+the equality rules on inductive types and constructors. 
+
+The module subtyping rules:
+\begin{itemize}
+\item [MSUB-SIG]
+\inference{%
+  \frac{
+    \begin{array}{c}
+      \WS{E;\Spec_1;\dots;\Spec_n}{\Spec_i}{\Spec'_{\sigma(i)}} 
+                                  \textrm{ \ for } i=1..n \\
+      \sigma : \{1\dots n\} \ra \{1\dots m\} \textrm{ \ injective}
+    \end{array}
+  }{
+    \WS{E}{\sig{\Spec_1;\dots;\Spec_n}}{\sig{\Spec'_1;\dots;\Spec'_m}}
+  }
+}
+\item [MSUB-FUN]
+\inference{%       T_1 -> T_2 <: T_1' -> T_2'
+  \frac{
+    \WS{E}{T_1'}{T_1}~~~~~~~~~~\WS{E;\ModS{X}{T_1'}}{T_2}{T_2'}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WS{E}{\funsig{X}{T_1}{T_2}}{\funsig{X}{T_1'}{T_2'}}
+  }
+}
+\item [MSUB-EQ]
+\inference{%
+  \frac{
+    \WS{E}{T_1}{T_2}~~~~~~~~~~\WTERED{}{T_1}{=}{T_1'}~~~~~~~~~~\WTERED{}{T_2}{=}{T_2'}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WS{E}{T_1'}{T_2'}
+  }
+}
+\item [MSUB-REFL]
+\inference{%
+  \frac{
+    \WFT{E}{T}
+  }{
+    \WS{E}{T}{T}
+  }
+}
+\end{itemize}
+Specification subtyping rules:
+\begin{itemize}
+\item [ASSUM-ASSUM]
+\inference{%
+  \frac{
+    \WTELECONV{}{U_1}{U_2}
+  }{
+    \WSE{\Assum{}{c}{U_1}}{\Assum{}{c}{U_2}}
+  }
+}
+\item [DEF-ASSUM]
+\inference{%
+  \frac{
+    \WTELECONV{}{U_1}{U_2}
+  }{
+    \WSE{\Def{}{c}{U_1}{t}}{\Assum{}{c}{U_2}}
+  }
+}
+\item [ASSUM-DEF]
+\inference{%
+  \frac{
+    \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{c}{t_2}
+  }{
+    \WSE{\Assum{}{c}{U_1}}{\Def{}{c}{U_2}{t_2}}
+  }
+}
+\item [DEF-DEF]
+\inference{%
+  \frac{
+    \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
+  }{
+    \WSE{\Def{}{c}{U_1}{t_1}}{\Def{}{c}{U_2}{t_2}}
+  }
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\item [MODS-MODS]
+\inference{%
+  \frac{
+    \WSE{T_1}{T_2}
+  }{
+    \WSE{\ModS{m}{T_1}}{\ModS{m}{T_2}}
+  }
+}
+\item [MODEQ-MODS]
+\inference{%
+  \frac{
+    \WSE{T_1}{T_2}
+  }{
+    \WSE{\ModSEq{m}{T_1}{p}}{\ModS{m}{T_2}}
+  }
+}
+\item [MODS-MODEQ]
+\inference{%
+  \frac{
+    \WSE{T_1}{T_2}~~~~~~~~\WTERED{}{m}{=}{p_2}
+  }{
+    \WSE{\ModS{m}{T_1}}{\ModSEq{m}{T_2}{p_2}}
+  }
+}
+\item [MODEQ-MODEQ]
+\inference{%
+  \frac{
+    \WSE{T_1}{T_2}~~~~~~~~\WTERED{}{p_1}{=}{p_2}
+  }{
+    \WSE{\ModSEq{m}{T_1}{p_1}}{\ModSEq{m}{T_2}{p_2}}
+  }
+}
+\item [MODTYPE-MODTYPE]
+\inference{%
+  \frac{
+    \WSE{T_1}{T_2}~~~~~~~~\WSE{T_2}{T_1}
+  }{
+    \WSE{\ModType{S}{T_1}}{\ModType{S}{T_2}}
+  }
+}
+\end{itemize}
+Verification of the specification
+\begin{itemize}
+\item [IMPL-SPEC]
+\inference{%
+  \frac{
+    \begin{array}{c}
+      \WF{E;\Spec}{}\\
+      \Spec \textrm{\ is one of } {\sf Def, Assum, Ind, ModType}
+    \end{array}
+  }{
+    \WTE{}{\Spec}{\Spec}
+  }
+}
+\item [MOD-MODS]
+\inference{%
+  \frac{
+    \WF{E;\ModS{m}{T}}{}~~~~~~~~\WTE{}{M}{T}
+  }{
+    \WTE{}{\Mod{m}{T}{M}}{\ModS{m}{T}}
+  }
+}
+\item [MOD-MODEQ]
+\inference{%
+  \frac{
+    \WF{E;\ModSEq{m}{T}{p}}{}~~~~~~~~~~~\WTERED{}{p}{=}{p'}
+  }{
+    \WTE{}{\Mod{m}{T}{p'}}{\ModSEq{m}{T}{p'}}
+  }
+}
+
+\end{itemize}
+New environment formation rules
+\begin{itemize}
+\item [WF-MODS]
+\inference{%
+  \frac{
+    \WF{E}{}~~~~~~~~\WFT{E}{T}
+  }{
+    \WF{E;\ModS{m}{T}}{}
+  }
+}
+\item [WF-MODEQ]
+\inference{%
+  \frac{
+    \WF{E}{}~~~~~~~~~~~\WTE{}{p}{T}
+  }{
+    \WF{E,\ModSEq{m}{T}{p}}{}
+  }
+}
+\item [WF-MODTYPE]
+\inference{%
+  \frac{
+    \WF{E}{}~~~~~~~~~~~\WFT{E}{T}
+  }{
+    \WF{E,\ModType{S}{T}}{}
+  }
+}
+\item [WF-IND]
+\inference{%
+  \frac{
+    \begin{array}{c}
+      \WF{E;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}{}\\
+      \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'};\dots}}\\
+      \WS{E}{\subst{\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}{p.l}{l}_{l
+      \in \lab{Spec_1;\dots;Spec_n}}}{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}
+    \end{array}
+  }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}\\
+  }
+}
+\end{itemize}
+Component access rules
+\begin{itemize}
+\item [ACC-TYPE]
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Assum{}{c}{U};\dots}}
+  }{
+    \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\item []
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
+  }{
+    \WTEG{p.c}{\subst{U}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\item[] Notice that the following rule extends the delta rule defined in
+section~\ref{delta}
+\item [ACC-DELTA]
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
+  }{
+    \WTEGRED{p.c}{\triangleright_\delta}{\subst{t}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\item [] in the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
+  $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
+  $[c_1:C_1;\ldots;c_n:C_n]$
+\item [ACC-IND]
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
+  }{
+    \WTEG{p.I_j}{\subst{(p_1:P_1)\ldots(p_r:P_r)A_j}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
+  }{
+    \WTEG{p.c_m}{\subst{(p_1:P_1)\ldots(p_r:P_r)\subst{C_m}{I_j}{(I_j~p_1\ldots
+       p_r)}_{j=1\ldots k}}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\item [ACC-INDP]
+\inference{%
+  \frac{
+    \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
+  }{
+    \WTRED{E}{}{p.I_i}{\triangleright_\delta}{p'.I_i}
+  }
+}
+\inference{%
+  \frac{
+    \WT{E}{}{p:\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
+  }{
+    \WTRED{E}{}{p.c_i}{\triangleright_\delta}{p'.c_i}
+  }
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%% MODULES
+\item [ACC-MOD]
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModS{m}{T};\dots}}
+  }{
+    \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\item []
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModSEq{m}{T}{p'};\dots}}
+  }{
+    \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\item [ACC-MODEQ]
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModSEq{m}{T}{p'};\dots}}
+  }{
+    \WTEGRED{p.m}{=}{\subst{p'}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\item [ACC-MODTYPE]
+\inference{%
+  \frac{
+    \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModType{S}{T};\dots}}
+  }{
+    \WTEGRED{p.S}{=}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
+  }
+}
+\end{itemize}
+The function $\lab{}$ is used to calculate the set of label of
+the set of specifications. It is defined by
+$\lab{\Spec_1;\dots;\Spec_n}=\lab{\Spec_1}\cup\dots;\cup\lab{\Spec_n}$
+where $\lab{\Spec}$ is defined as follows:
+\begin{itemize}
+\item $\lab{\Assum{\Gamma}{c}{U}}=\{c\}$,
+\item $\lab{\Def{\Gamma}{c}{U}{t}}=\{c\}$,
+\item
+  $\lab{\Ind{\Gamma}{\Gamma_P}{\Gamma_C}{\Gamma_I}}=\dom{\Gamma_C}\cup\dom{\Gamma_I}$,
+\item $\lab{\ModS{m}{T}}=\{m\}$,
+\item $\lab{\ModSEq{m}{T}{M}}=\{m\}$,
+\item $\lab{\ModType{S}{T}}=\{S\}$
+\end{itemize}
+Environment access for modules and module types
+\begin{itemize}
+\item [ENV-MOD]
+\inference{%
+  \frac{
+    \WF{E;\ModS{m}{T};E'}{\Gamma}
+  }{
+    \WT{E;\ModS{m}{T};E'}{\Gamma}{m}{T}
+  }
+}
+\item []
+\inference{%
+  \frac{
+    \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
+  }{
+    \WT{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{T}
+  }
+}
+\item [ENV-MODEQ]
+\inference{%
+  \frac{
+    \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
+  }{
+    \WTRED{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{=}{p}
+  }
+}
+\item [ENV-MODTYPE]
+\inference{%
+  \frac{
+    \WF{E;\ModType{S}{T};E'}{\Gamma}
+  }{
+    \WTRED{E;\ModType{S}{T};E'}{\Gamma}{S}{=}{T}
+  }
+}
+\item [ENV-INDP]
+\inference{%
+  \frac{
+    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
+  }{
+    \WTRED{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}{I_i}{\triangleright_\delta}{p.I_i}
+  }
+}
+\inference{%
+  \frac{
+    \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
+  }{
+    \WTRED{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}{c_i}{\triangleright_\delta}{p.c_i}
+  }
+}
+\end{itemize}
+Module path equality is a transitive and reflexive closure of the
+relation generated by ACC-MODEQ and ENV-MODEQ.
+\begin{itemize}
+\item [MP-EQ-REFL]
+\inference{%
+  \frac{
+    \WTEG{p}{T}
+  }{
+    \WTEG{p}{p}
+  }
+}
+\item [MP-EQ-TRANS]
+\inference{%
+  \frac{
+    \WTEGRED{p}{=}{p'}~~~~~~\WTEGRED{p'}{=}{p''}
+  }{
+    \WTEGRED{p'}{=}{p''}
+  }
+}
+
+\end{itemize}
+
+
+% $Id$
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
+
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 49483e3d3e..225c724a16 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -8,7 +8,7 @@
 
 \makeatletter
 
-%\includeonly{RefMan-syn.v,Cases.v,Coercion.v}
+%\includeonly{RefMan-cic.v,RefMan-ext.v}
 
 \input{./macros.tex}% extension .tex pour htmlgen
 \input{./title.tex}% extension .tex pour htmlgen
@@ -33,6 +33,9 @@
 \include{RefMan-lib.v}% The coq library
 \include{RefMan-cic.v}% The Calculus of Constructions
 
+\include{RefMan-modr.tex}% The module system
+
+
 \part{The proof engine}
 \include{RefMan-oth.v}% Vernacular commands
 \include{RefMan-pro}% Proof handling
diff --git a/doc/macros.tex b/doc/macros.tex
index c70ad240f4..7a898a2d38 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -144,6 +144,10 @@
 \newcommand{\terms}{\textrm{\textsl{terms}}}
 \newcommand{\term}{\textrm{\textsl{term}}}
 \newcommand{\module}{\textrm{\textsl{module}}}
+\newcommand{\modexpr}{\textrm{\textsl{module\_expression}}}
+\newcommand{\modtype}{\textrm{\textsl{module\_type}}}
+\newcommand{\onemodbinding}{\textrm{\textsl{module\_binding}}}
+\newcommand{\modbindings}{\textrm{\textsl{module\_bindings}}}
 \newcommand{\qualid}{\textrm{\textsl{qualid}}}
 \newcommand{\class}{\textrm{\textsl{class}}}
 \newcommand{\dirpath}{\textrm{\textsl{dirpath}}}
@@ -274,18 +278,28 @@
 \newcommand{\sumbool}[2]{\{#1\}+\{#2\}}
 \newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3}
 \newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2}
-\newcommand{\WF}[2]{\mbox{${\cal W\!F}(#1)[#2]$}}
+\newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}}
 \newcommand{\WFE}[1]{\WF{E}{#1}}
-\newcommand{\WT}[4]{\mbox{$#1[#2] \vdash #3 : #4$}}
+\newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}}
 \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
 \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
 
+\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}}
+\newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\cal W\!F}(#2)}}
+\newcommand{\WS}[3]{\ensuremath{#1[] \vdash #2 <: #3}}
+\newcommand{\WSE}[2]{\WS{E}{#1}{#2}}
+
+\newcommand{\WTRED}[5]{\mbox{$#1[#2] \vdash #3 #4 #5$}}
 \newcommand{\WTERED}[4]{\mbox{$E[#1] \vdash #2 #3 #4$}}
 \newcommand{\WTELECONV}[3]{\WTERED{#1}{#2}{\leconvert}{#3}}
 \newcommand{\WTEGRED}[3]{\WTERED{\Gamma}{#1}{#2}{#3}}
+\newcommand{\WTECONV}[3]{\WTERED{#1}{#2}{\convert}{#3}}
 \newcommand{\WTEGCONV}[2]{\WTERED{\Gamma}{#1}{\convert}{#2}}
 \newcommand{\WTEGLECONV}[2]{\WTERED{\Gamma}{#1}{\leconvert}{#2}}
 
+\newcommand{\lab}[1]{\mathit{labels}(#1)}
+\newcommand{\dom}[1]{\mathit{dom}(#1)}
+
 \newcommand{\CI}[2]{\mbox{$\{#1\}^{#2}$}}
 \newcommand{\CIP}[3]{\mbox{$\{#1\}_{#2}^{#3}$}}
 \newcommand{\CIPV}[1]{\CIP{#1}{I_1.. I_k}{P_1.. P_k}}
@@ -295,6 +309,8 @@
                                               \,)\end{array}$}}
 \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{l}#3:=#4
                                                  \,)\end{array}$}}
+\newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{l}#3:=#4
+                                                 \,)\end{array}$}}
 \newcommand{\Def}[4]{\mbox{{\sf Def}$(#1)(#2:=#3:#4)$}}
 \newcommand{\Assum}[3]{\mbox{{\sf Assum}$(#1)(#2:#3)$}}
 \newcommand{\Match}[3]{\mbox{$<\!#1\!>\!{\mbox{\tt Match}}~#2~{\mbox{\tt with}}~#3~{\mbox{\tt end}}$}}
@@ -312,6 +328,17 @@
 \newcommand{\compat}[2]{\mbox{$[#1|#2]$}}
 \newcommand{\tristackrel}[3]{\mathrel{\mathop{#2}\limits_{#3}^{#1}}}
 
+\newcommand{\Impl}{{\it Impl}}
+\newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}:={#3})}
+\newcommand{\ModType}[2]{{\sf ModType}({#1}:={#2})}
+\newcommand{\ModS}[2]{{\sf ModS}({#1}:{#2})}
+\newcommand{\ModSEq}[3]{{\sf ModSEq}({#1}:{#2}=={#3})}
+\newcommand{\functor}[3]{\ensuremath{{\sf Functor}[#1:#2]\;#3}}
+\newcommand{\funsig}[3]{\ensuremath{{\sf Funsig}(#1:#2)\;#3}}
+\newcommand{\sig}[1]{\ensuremath{{\sf Sig}~#1~{\sf End}}}
+\newcommand{\struct}[1]{\ensuremath{{\sf Struct}~#1~{\sf End}}}
+
+
 \newbox\tempa
 \newbox\tempb
 \newdimen\tempc