Mis-a-jour modules, ajout de Import et Export

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

4 files changed, 209 insertions, 122 deletions

diff --git a/doc/RefMan-mod.tex b/doc/RefMan-mod.tex
index d6d53b4209..de4f14fa51 100644
--- a/doc/RefMan-mod.tex
+++ b/doc/RefMan-mod.tex
@@ -1,4 +1,4 @@
-\section{Module system}
+\section{Module system}\index{Modules}\label{Modules}
 
 The module system provides a way of packaging related elements
 together, as well as a mean of massive abstraction.
@@ -140,11 +140,11 @@ only in module types.
 Let us define a simple module.
 \begin{coq_example}
 Module M.
-Definition T := nat.
-Definition x := 0.
-Definition y : bool.
-  exact true.
-Defined.
+  Definition T := nat.
+  Definition x := 0.
+  Definition y : bool.
+    exact true.
+  Defined.
 End M.
 \end{coq_example}
 
@@ -159,8 +159,8 @@ Print M.x.
 A simple module type:
 \begin{coq_example}
 Module Type SIG.
-Parameter T : Set.
-Parameter x : T.
+  Parameter T : Set.
+  Parameter x : T.
 End SIG.
 \end{coq_example}
 
@@ -175,7 +175,7 @@ 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.
+Module N  :  SIG with Definition T := nat  :=  M.
 Print N.T.
 Print N.x.
 Print N.y.
@@ -191,8 +191,8 @@ one:
 
 \begin{coq_example*}
 Module Type SIG'.
-Definition T : Set := nat.
-Parameter x : T.
+  Definition T : Set := nat.
+  Parameter x : T.
 End SIG'.
 Module N : SIG' := M.
 \end{coq_example*}
@@ -208,8 +208,8 @@ Now let us create a functor, i.e.\ a parametric module
 Module Two (X Y: SIG).
 \end{coq_example}
 \begin{coq_example*}
-Definition T := X.T * Y.T.
-Definition x := (X.x, Y.x).
+  Definition T := X.T * Y.T.
+  Definition x := (X.x, Y.x).
 \end{coq_example*}
 \begin{coq_example}
 End Two.
@@ -223,24 +223,27 @@ In the end, let us define a module type with two sub-modules, sharing
 some of the fields and give one of its possible implementations:
 \begin{coq_example}
 Module Type SIG2.
-Declare Module M1 : SIG.
-Declare Module M2 <: SIG.
-Definition T := M1.T.
-Parameter x : T.
-End M2.
+  Declare Module M1 : SIG.
+  Declare Module M2 <: SIG.
+    Definition T := M1.T.
+    Parameter x : T.
+  End M2.
 End SIG2.
 \end{coq_example}
 \begin{coq_example*}
 Module Mod <: SIG2.
-Module M1.
-Definition T := nat.
-Definition x := 1.
-End M1.
-Module M2 := M.
+  Module M1.
+    Definition T := nat.
+    Definition x := 1.
+  End M1.
+  Module M2 := M.
 \end{coq_example*}
 \begin{coq_example}
 End Mod.
 \end{coq_example}
+Notice that \texttt{M} is a correct body for the component \texttt{M2}
+since its \texttt{T} component is equal \texttt{nat} and hence
+\texttt{M1.T} as specified.
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
@@ -274,6 +277,46 @@ Reset Initial.
 
 \end{Remarks}
 
+\subsection{Import {\qualid}}\comindex{Import}\label{Import}
+If {\qualid} denotes a valid basic module (i.e. its module type is a
+signature), makes its components available by their short names.
+
+Example:
+
+\begin{coq_example}
+Module Mod.
+\end{coq_example}
+\begin{coq_example}
+  Definition T:=nat.
+  Check T.
+\end{coq_example}
+\begin{coq_example}
+End Mod.
+Check Mod.T.
+Check T. (* Incorrect ! *)
+Import Mod.
+Check T. (* Now correct *)
+\end{coq_example}
+\begin{coq_eval}
+Reset Mod.
+\end{coq_eval}
+
+
+\begin{Variants}
+\item{\tt Export {\qualid}}\comindex{Export}\\
+  When the module containing the command {\tt Export {\qualid}} is
+  imported, {\qualid} is imported as well.
+\end{Variants}
+
+\begin{ErrMsgs}
+  \item \errindex{{\qualid} is not a module}
+% this error is impossible in the import command
+%  \item \errindex{Cannot mask the absolute name {\qualid} !}
+\end{ErrMsgs}
+\begin{Warnings}
+  \item Warning: Trying to mask the absolute name {\qualid} !
+\end{Warnings}
+
 \subsection{\tt Print Module {\ident}}\comindex{Print Module}
 Prints the module type and (optionally) the body of the module {\ident}.
 
diff --git a/doc/RefMan-modr.tex b/doc/RefMan-modr.tex
index 47699df601..c5f3097635 100644
--- a/doc/RefMan-modr.tex
+++ b/doc/RefMan-modr.tex
@@ -4,6 +4,7 @@
 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.
+%It is described in details in Judicael's thesis and Jacek's thesis
 
 \section{Modules and module types}
 
@@ -28,7 +29,7 @@ or a definition of a module or a module type abbreviation.
 specification of a constant, an assumption, an inductive, a module or
 a module type abbreviation.
 
-\paragraph{Module type}, denoted by $T$ can be:
+\paragraph{Module type,} denoted by $T$ can be:
 \begin{itemize}
 \item a module type name
 \item an access path $p$
@@ -37,29 +38,29 @@ a module type abbreviation.
   module types
 \end{itemize}
 
-\paragraph{Module definition}, written $\Mod{X}{T}{M}$ can be a
+\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
+\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
+\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
+In order to introduce the typing system we 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.
+constants and inductives now also hold any other signature elements.
+Terms, apart from variables, constants and complex terms, 
+include also access paths.
 
-We will also need additional typing judgments: 
+We also need additional typing judgments: 
 \begin{itemize}
 \item \WFT{E}{T}, denoting that a module type $T$ is well-formed, 
 
@@ -77,7 +78,7 @@ module type $T_2$.
 \end{itemize}
 The rules for forming module types are the following:
 \begin{itemize}
-\item [WF-SIG]
+\item [] WF-SIG
 \inference{%
   \frac{
     \WF{E;E'}{}
@@ -85,7 +86,7 @@ The rules for forming module types are the following:
     \WFT{E}{\sig{E'}}
   }
 }
-\item [WF-FUN]
+\item [] WF-FUN
 \inference{%
   \frac{
     \WFT{E;\ModS{X}{T}}{T'}
@@ -96,7 +97,7 @@ The rules for forming module types are the following:
 \end{itemize}
 Rules for typing module expressions:
 \begin{itemize}
-\item [MT-STRUCT]
+\item [] MT-STRUCT
 \inference{%
   \frac{
     \begin{array}{c}
@@ -108,7 +109,7 @@ Rules for typing module expressions:
     \WTM{E}{\struct{\Impl_1;\dots;\Impl_n}}{\sig{\Spec_1;\dots;\Spec_n}}
   }
 }
-\item [MT-FUN]
+\item [] MT-FUN
 \inference{%
   \frac{
     \WTM{E;\ModS{X}{T}}{M}{T'}
@@ -116,15 +117,19 @@ Rules for typing module expressions:
     \WTM{E}{\functor{X}{T}{M}}{\funsig{X}{T}{T'}}
   }
 }
-\item [MT-APP]
+\item [] MT-APP
 \inference{%
   \frac{
-    \WTM{E}{p'}{\funsig{X}{T}{T'}}~~~~~~~~~~~\WTM{E}{p''}{T}
+    \begin{array}{c}
+      \WTM{E}{p}{\funsig{X_1}{T_1}{\!\dots\funsig{X_n}{T_n}{T'}}}\\
+      \WTM{E}{p_i}{T_i\{X_1/p_1\dots X_{i-1}/p_{i-1}\}}
+                                   \textrm{ \ \ for } i=1\dots n
+    \end{array}
   }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-    \WTM{E}{p' p''}{T'\{X/p''\}}
+    \WTM{E}{p\; p_1 \dots p_n}{T'\{X_1/p_1\dots X_n/p_n\}}
   }
 }
-\item [MT-SUB]
+\item [] MT-SUB
 \inference{%
   \frac{
     \WTM{E}{M}{T}~~~~~~~~~~~~\WS{E}{T}{T'}
@@ -132,7 +137,7 @@ Rules for typing module expressions:
     \WTM{E}{M}{T'}
   }
 }
-\item [MT-STR]
+\item [] MT-STR
 \inference{%
   \frac{
     \WTM{E}{p}{T}
@@ -152,11 +157,11 @@ meaning:
   \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 $\ModSEq{X}{T}{p'}/p ~=~ \ModSEq{X}{T/p}{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=\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}
@@ -170,19 +175,19 @@ the equality rules on inductive types and constructors.
 
 The module subtyping rules:
 \begin{itemize}
-\item [MSUB-SIG]
+\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}
+      \WS{E;\Spec_1;\dots;\Spec_n}{\Spec_{\sigma(i)}}{\Spec'_i}
+                                  \textrm{ \ for } i=1..m \\
+      \sigma : \{1\dots m\} \ra \{1\dots n\} \textrm{ \ injective}
     \end{array}
   }{
     \WS{E}{\sig{\Spec_1;\dots;\Spec_n}}{\sig{\Spec'_1;\dots;\Spec'_m}}
   }
 }
-\item [MSUB-FUN]
+\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'}
@@ -190,26 +195,27 @@ The module subtyping rules:
     \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}
-  }
-}
+% these are derived rules
+% \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]
+\item []ASSUM-ASSUM
 \inference{%
   \frac{
     \WTELECONV{}{U_1}{U_2}
@@ -217,7 +223,7 @@ Specification subtyping rules:
     \WSE{\Assum{}{c}{U_1}}{\Assum{}{c}{U_2}}
   }
 }
-\item [DEF-ASSUM]
+\item []DEF-ASSUM
 \inference{%
   \frac{
     \WTELECONV{}{U_1}{U_2}
@@ -225,7 +231,7 @@ Specification subtyping rules:
     \WSE{\Def{}{c}{U_1}{t}}{\Assum{}{c}{U_2}}
   }
 }
-\item [ASSUM-DEF]
+\item []ASSUM-DEF
 \inference{%
   \frac{
     \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{c}{t_2}
@@ -233,7 +239,7 @@ Specification subtyping rules:
     \WSE{\Assum{}{c}{U_1}}{\Def{}{c}{U_2}{t_2}}
   }
 }
-\item [DEF-DEF]
+\item []DEF-DEF
 \inference{%
   \frac{
     \WTELECONV{}{U_1}{U_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
@@ -241,8 +247,42 @@ Specification subtyping rules:
     \WSE{\Def{}{c}{U_1}{t_1}}{\Def{}{c}{U_2}{t_2}}
   }
 }
+\item []IND-IND
+\inference{%
+  \frac{
+    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
+    ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
+    ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
+  }{
+    \WSE{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}%
+        {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
+  }
+}
+\item []INDP-IND
+\inference{%
+  \frac{
+    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
+    ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
+    ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
+  }{
+    \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
+        {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
+  }
+}
+\item []INDP-INDP
+\inference{%
+  \frac{
+    \WTECONV{}{\Gamma_P}{\Gamma_P'}%
+    ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
+    ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
+    ~~~~~~~~\WTECONV{}{p}{p'}
+  }{
+    \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
+        {\Indp{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}{p'}}
+  }
+}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\item [MODS-MODS]
+\item []MODS-MODS
 \inference{%
   \frac{
     \WSE{T_1}{T_2}
@@ -250,7 +290,7 @@ Specification subtyping rules:
     \WSE{\ModS{m}{T_1}}{\ModS{m}{T_2}}
   }
 }
-\item [MODEQ-MODS]
+\item []MODEQ-MODS
 \inference{%
   \frac{
     \WSE{T_1}{T_2}
@@ -258,23 +298,23 @@ Specification subtyping rules:
     \WSE{\ModSEq{m}{T_1}{p}}{\ModS{m}{T_2}}
   }
 }
-\item [MODS-MODEQ]
+\item []MODS-MODEQ
 \inference{%
   \frac{
-    \WSE{T_1}{T_2}~~~~~~~~\WTERED{}{m}{=}{p_2}
+    \WSE{T_1}{T_2}~~~~~~~~\WTECONV{}{m}{p_2}
   }{
     \WSE{\ModS{m}{T_1}}{\ModSEq{m}{T_2}{p_2}}
   }
 }
-\item [MODEQ-MODEQ]
+\item []MODEQ-MODEQ
 \inference{%
   \frac{
-    \WSE{T_1}{T_2}~~~~~~~~\WTERED{}{p_1}{=}{p_2}
+    \WSE{T_1}{T_2}~~~~~~~~\WTECONV{}{p_1}{p_2}
   }{
     \WSE{\ModSEq{m}{T_1}{p_1}}{\ModSEq{m}{T_2}{p_2}}
   }
 }
-\item [MODTYPE-MODTYPE]
+\item []MODTYPE-MODTYPE
 \inference{%
   \frac{
     \WSE{T_1}{T_2}~~~~~~~~\WSE{T_2}{T_1}
@@ -285,7 +325,7 @@ Specification subtyping rules:
 \end{itemize}
 Verification of the specification
 \begin{itemize}
-\item [IMPL-SPEC]
+\item []IMPL-SPEC
 \inference{%
   \frac{
     \begin{array}{c}
@@ -296,7 +336,7 @@ Verification of the specification
     \WTE{}{\Spec}{\Spec}
   }
 }
-\item [MOD-MODS]
+\item []MOD-MODS
 \inference{%
   \frac{
     \WF{E;\ModS{m}{T}}{}~~~~~~~~\WTE{}{M}{T}
@@ -304,10 +344,10 @@ Verification of the specification
     \WTE{}{\Mod{m}{T}{M}}{\ModS{m}{T}}
   }
 }
-\item [MOD-MODEQ]
+\item []MOD-MODEQ
 \inference{%
   \frac{
-    \WF{E;\ModSEq{m}{T}{p}}{}~~~~~~~~~~~\WTERED{}{p}{=}{p'}
+    \WF{E;\ModSEq{m}{T}{p}}{}~~~~~~~~~~~\WTECONV{}{p}{p'}
   }{
     \WTE{}{\Mod{m}{T}{p'}}{\ModSEq{m}{T}{p'}}
   }
@@ -316,7 +356,7 @@ Verification of the specification
 \end{itemize}
 New environment formation rules
 \begin{itemize}
-\item [WF-MODS]
+\item []WF-MODS
 \inference{%
   \frac{
     \WF{E}{}~~~~~~~~\WFT{E}{T}
@@ -324,7 +364,7 @@ New environment formation rules
     \WF{E;\ModS{m}{T}}{}
   }
 }
-\item [WF-MODEQ]
+\item []WF-MODEQ
 \inference{%
   \frac{
     \WF{E}{}~~~~~~~~~~~\WTE{}{p}{T}
@@ -332,7 +372,7 @@ New environment formation rules
     \WF{E,\ModSEq{m}{T}{p}}{}
   }
 }
-\item [WF-MODTYPE]
+\item []WF-MODTYPE
 \inference{%
   \frac{
     \WF{E}{}~~~~~~~~~~~\WFT{E}{T}
@@ -340,7 +380,7 @@ New environment formation rules
     \WF{E,\ModType{S}{T}}{}
   }
 }
-\item [WF-IND]
+\item []WF-IND
 \inference{%
   \frac{
     \begin{array}{c}
@@ -356,7 +396,7 @@ New environment formation rules
 \end{itemize}
 Component access rules
 \begin{itemize}
-\item [ACC-TYPE]
+\item []ACC-TYPE
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Assum{}{c}{U};\dots}}
@@ -374,7 +414,7 @@ Component access rules
 }
 \item[] Notice that the following rule extends the delta rule defined in
 section~\ref{delta}
-\item [ACC-DELTA]
+\item [] ACC-DELTA
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\Def{}{c}{U}{t};\dots}}
@@ -385,7 +425,7 @@ section~\ref{delta}
 \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]
+\item []ACC-IND
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;\Spec_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
@@ -401,7 +441,7 @@ section~\ref{delta}
        p_r)}_{j=1\ldots k}}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item [ACC-INDP]
+\item []ACC-INDP
 \inference{%
   \frac{
     \WT{E}{}{p}{\sig{\Spec_1;\dots;\Spec_n;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
@@ -417,7 +457,7 @@ section~\ref{delta}
   }
 }
 %%%%%%%%%%%%%%%%%%%%%%%%%%% MODULES
-\item [ACC-MOD]
+\item []ACC-MOD
 \inference{%
   \frac{
     \WTEG{p}{\sig{\Spec_1;\dots;Spec_i;\ModS{m}{T};\dots}}
@@ -433,20 +473,20 @@ section~\ref{delta}
     \WTEG{p.m}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item [ACC-MODEQ]
+\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}}}
+    \WTEGRED{p.m}{\triangleright_\delta}{\subst{p'}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
-\item [ACC-MODTYPE]
+\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}}}
+    \WTEGRED{p.S}{\triangleright_\delta}{\subst{T}{p.l}{l}_{l \in \lab{Spec_1;\dots;Spec_i}}}
   }
 }
 \end{itemize}
@@ -465,7 +505,7 @@ where $\lab{\Spec}$ is defined as follows:
 \end{itemize}
 Environment access for modules and module types
 \begin{itemize}
-\item [ENV-MOD]
+\item []ENV-MOD
 \inference{%
   \frac{
     \WF{E;\ModS{m}{T};E'}{\Gamma}
@@ -481,23 +521,23 @@ Environment access for modules and module types
     \WT{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{T}
   }
 }
-\item [ENV-MODEQ]
+\item []ENV-MODEQ
 \inference{%
   \frac{
     \WF{E;\ModSEq{m}{T}{p};E'}{\Gamma}
   }{
-    \WTRED{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{=}{p}
+    \WTRED{E;\ModSEq{m}{T}{p};E'}{\Gamma}{m}{\triangleright_\delta}{p}
   }
 }
-\item [ENV-MODTYPE]
+\item []ENV-MODTYPE
 \inference{%
   \frac{
     \WF{E;\ModType{S}{T};E'}{\Gamma}
   }{
-    \WTRED{E;\ModType{S}{T};E'}{\Gamma}{S}{=}{T}
+    \WTRED{E;\ModType{S}{T};E'}{\Gamma}{S}{\triangleright_\delta}{T}
   }
 }
-\item [ENV-INDP]
+\item []ENV-INDP
 \inference{%
   \frac{
     \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
@@ -513,27 +553,28 @@ Environment access for modules and module types
   }
 }
 \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''}
-  }
-}
+% %%% replaced by \triangle_\delta
+% 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}
+% \end{itemize}
 
 
 % $Id$
diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index d420a269af..6a5dc3958e 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -419,10 +419,13 @@ waste of time.
 % \SeeAlso sections \ref{Opaque}, \ref{loadpath}, chapter
 % \ref{Addoc-coqc}
 
-\subsection{\tt Import {\qualid}.}\comindex{Import}
-\label{Import}
+%\subsection{\tt Import {\qualid}.}\comindex{Import}
+%\label{Import}
 
-TODO + variant Export
+%%%%%%%%%%%%
+% Import and Export described in RefMan-mod.tex
+% the minor difference (to avoid multiple Exporting of libraries) in
+% the treatment of normal modules and libraries by Export omitted
 
 
 \subsection{\tt Require {\dirpath}.}
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index f272a04f6d..8eb7f3eb08 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -17,7 +17,7 @@
 \fi
 
 
-%\includeonly{RefMan-cic.v,RefMan-ext.v}
+%\includeonly{RefMan-cic.v,RefMan-ext.v,RefMan-modr}
 
 \input{./version.tex}
 \input{./macros.tex}% extension .tex pour htmlgen