1 files changed, 0 insertions, 411 deletions
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
deleted file mode 100644
index 68d57226..00000000
--- a/doc/refman/RefMan-mod.tex
+++ /dev/null
@@ -1,411 +0,0 @@
-\section{Module system
-\index{Modules}
-\label{section:Modules}}
-
-The module system provides a way of packaging related elements
-together, as well as a mean of massive abstraction.
-
-\begin{figure}[t]
-\begin{centerframe}
-\begin{tabular}{rcl}
-{\modtype}  & ::= & {\qualid} \\
- & $|$ & {\modtype} \texttt{ with Definition }{\qualid} := {\term} \\
- & $|$ & {\modtype} \texttt{ with Module }{\qualid} := {\qualid} \\
- & $|$ & {\qualid} \nelist{\qualid}{}\\
- & $|$ & $!${\qualid} \nelist{\qualid}{}\\
- &&\\
-
-{\onemodbinding}  & ::= & {\tt ( [Import|Export] \nelist{\ident}{} : {\modtype} )}\\
- &&\\
-
-{\modbindings} & ::= & \nelist{\onemodbinding}{}\\
- &&\\
-
-{\modexpr} & ::= & \nelist{\qualid}{} \\
-           & $|$ & $!$\nelist{\qualid}{}
-\end{tabular}
-\end{centerframe}
-\caption{Syntax of modules}
-\end{figure}
-
-In the syntax of module application, the $!$ prefix indicates that
-any {\tt Inline} directive in the type of the functor arguments
-will be ignored (see \ref{Inline} below).
-
-\subsection{\tt Module {\ident}
-\comindex{Module}}
-
-This command is used to start an interactive module named {\ident}.
-
-\begin{Variants}
-
-\item{\tt Module {\ident} {\modbindings}}
-
-  Starts an interactive functor with parameters given by {\modbindings}.
-
-\item{\tt Module {\ident} \verb.:. {\modtype}}
-
-  Starts an interactive module specifying its module type. 
-
-\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype}}
-
-  Starts an interactive functor with parameters given by
-  {\modbindings}, and output module type {\modtype}.
-
-\item{\tt Module {\ident} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:.{ \modtype$_n$}}
-
-  Starts an interactive module satisfying each {\modtype$_i$}. 
-
-\item{\tt Module {\ident} {\modbindings} \verb.<:. {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:. {\modtype$_n$}}
-
-  Starts an interactive functor with parameters given by
-  {\modbindings}. The output module type is verified against each
-  module type {\modtype$_i$}.
-
-\item\texttt{Module [Import|Export]}
-
-  Behaves like \texttt{Module}, but automatically imports or exports
-  the module.
-
-\end{Variants}
-\subsubsection{Reserved commands inside an interactive module:
-\comindex{Include}}
-\begin{enumerate}
-\item {\tt Include {\module}}
-
-  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 {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
-
-is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
-\end{enumerate}
-\subsection{\tt End {\ident}
-\comindex{End}}
-
-This command closes the interactive 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) its components (constants, inductive types, 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}.
-
-% Particular cases of the next 2 items
-%\item{\tt Module {\ident} \verb.:. {\modtype} := {\modexpr}}
-%
-%  Defines a module with body {\modexpr} and interface {\modtype}.
-%\item{\tt Module {\ident} \verb.<:. {\modtype} := {\modexpr}}
-%
-%  Defines a module with body {\modexpr}, satisfying {\modtype}.
-
-\item{\tt Module {\ident} {\modbindings} \verb.:. {\modtype} :=
-    {\modexpr}}
-
-  Defines a functor with parameters given by {\modbindings} (possibly none),
-  and output module type {\modtype}, with body {\modexpr}. 
-
-\item{\tt Module {\ident} {\modbindings} \verb.<:.  {\modtype$_1$} \verb.<:. $\ldots$ \verb.<:. {\modtype$_n$}:=
-    {\modexpr}}
-
-  Defines a functor with parameters given by {\modbindings} (possibly none) 
-  with body {\modexpr}. The body is checked against each {\modtype$_i$}.
-
-\item{\tt Module {\ident} {\modbindings} := {\modexpr$_1$} \verb.<+. $\ldots$ \verb.<+. {\modexpr$_n$}}
-
-  is equivalent to an interactive module where each {\modexpr$_i$} are included.
-
-\end{Variants}
-
-\subsection{\tt Module Type {\ident}
-\comindex{Module Type}}
-
-This command is used to start an interactive module type {\ident}.
-
-\begin{Variants}
-
-\item{\tt Module Type {\ident} {\modbindings}}
-
-  Starts an interactive functor type with parameters given by {\modbindings}.
-
-\end{Variants}
-\subsubsection{Reserved commands inside an interactive module type:
-\comindex{Include}\comindex{Inline}}
-\label{Inline}
-\begin{enumerate}
-\item {\tt Include {\module}}
-
- Same as {\tt Include} inside a module.
-
-\item {\tt Include {\module$_1$} \verb.<+. $\ldots$ \verb.<+. {\module$_n$}} 
-
-is a shortcut for {\tt Include {\module$_1$}}  $\ldots$ {\tt Include {\module$_n$}}
-
-\item {\tt {\assumptionkeyword} Inline {\assums} }
-
- The instance of this assumption will be automatically expanded at functor
- application, except when this functor application is prefixed by a $!$ annotation.
-\end{enumerate}
-\subsection{\tt End {\ident}
-\comindex{End}}
-
-This command closes the interactive module type {\ident}.
-
-\begin{ErrMsgs}
-\item \errindex{This is not the last opened module type}
-\end{ErrMsgs}
-
-\subsection{\tt Module Type {\ident} := {\modtype}}
-
-Defines a module type {\ident} equal to {\modtype}.
-
-\begin{Variants}
-\item {\tt Module Type {\ident} {\modbindings} := {\modtype}}
-
-  Defines a functor type {\ident} specifying functors taking arguments
-  {\modbindings} and returning {\modtype}.
-
-\item{\tt Module Type {\ident} {\modbindings} := {\modtype$_1$} \verb.<+. $\ldots$ \verb.<+. {\modtype$_n$}}
-
-  is equivalent to an interactive module type were each {\modtype$_i$} are included.
-
-\end{Variants}
-
-\subsection{\tt Declare Module {\ident} : {\modtype}}
-
-Declares a module {\ident} of type {\modtype}.
-
-\begin{Variants}
-
-\item{\tt Declare Module {\ident} {\modbindings} \verb.:. {\modtype}}
-
-  Declares a functor with parameters {\modbindings} and output module
-  type {\modtype}.
-
-
-\end{Variants}
-
-
-\subsubsection{Example}
-
-Let us define a simple module.
-\begin{coq_example}
-Module M.
-  Definition T := nat.
-  Definition x := 0.
-  Definition y : bool.
-    exact true.
-  Defined.
-End M.
-\end{coq_example}
-Inside a module one can define constants, prove theorems 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.
-  Parameter T : Set.
-  Parameter x : T.
-End SIG.
-\end{coq_example}
-
-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_eval}
-Set Printing Depth 50.
-(********** The following is not correct and should produce **********)
-(***************** Error: N.y not a defined object *******************)
-\end{coq_eval}
-\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}
-
-\noindent
-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.
-  Parameter x : T.
-End SIG'.
-Module N : SIG' := M.
-\end{coq_example*}
-If we just want to be sure that the our implementation satisfies a
-given module type without restricting the interface, we can use a
-transparent constraint
-\begin{coq_example}
-Module P <: SIG := M.
-Print P.y.
-\end{coq_example}
-Now let us create a functor, i.e. a parametric module
-\begin{coq_example}
-Module Two (X Y: SIG).
-\end{coq_example}
-\begin{coq_example*}
-  Definition T := (X.T * Y.T)%type.
-  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 Q := Two M N.
-Eval compute in (fst Q.x + snd Q.x).
-\end{coq_example}
-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.
-  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.
-\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}
-
-\begin{Remarks}
-\item Modules and module types can be nested components of each other.
-\item One can have sections inside a module or a module type, but
-  not a module or a module type inside a section.
-\item Commands like \texttt{Hint} or \texttt{Notation} can
-  also appear inside modules and module types. Note that in case of a
-  module definition like:
-
-    \smallskip
-    \noindent
-    {\tt Module N : SIG := M.} 
-    \smallskip
-
-    or
-
-    \smallskip
-    {\tt Module N : SIG.\\
-      \ \ \dots\\
-      End N.}
-    \smallskip 
-    
-    hints and the like valid for \texttt{N} are not those defined in
-    \texttt{M} (or the module body) but the ones defined in
-    \texttt{SIG}.
-
-\end{Remarks}
-
-\subsection{\tt 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}
-
-Some features defined in modules are activated only when a module is
-imported. This is for instance the case of notations (see
-Section~\ref{Notation}).
-
-\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 \errindexbis{{\qualid} is not a module}{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}.
-
-\subsection{\tt Print Module Type {\ident}
-\comindex{Print Module Type}}
-
-Prints the module type corresponding to {\ident}.
-
-\subsection{\tt Locate Module {\qualid}
-\comindex{Locate Module}}
-
-Prints the full name of the module {\qualid}.
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: