1 files changed, 0 insertions, 227 deletions
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
deleted file mode 100644
index f5178445..00000000
--- a/doc/refman/RefMan-uti.tex
+++ /dev/null
@@ -1,227 +0,0 @@
-\chapter[Utilities]{Utilities\label{Utilities}}
-
-The distribution provides utilities to simplify some tedious works
-beside proof development, tactics writing or documentation.
-
-\section[Building a toplevel extended with user tactics]{Building a toplevel extended with user tactics\label{Coqmktop}\index{Coqmktop@{\tt coqmktop}}}
-
-The native-code version of \Coq\ cannot dynamically load user tactics
-using Objective Caml code. It is possible to build a toplevel of \Coq,
-with Objective Caml code statically linked, with the tool {\tt
-  coqmktop}.
-
-For example, one can build a native-code \Coq\ toplevel extended with a tactic
-which source is in {\tt tactic.ml} with the command 
-\begin{verbatim}
-     % coqmktop -opt -o mytop.out tactic.cmx
-\end{verbatim}
-where {\tt tactic.ml} has been compiled with the native-code
-compiler {\tt ocamlopt}. This command generates an executable
-called {\tt mytop.out}. To use this executable to compile your \Coq\
-files, use {\tt coqc -image mytop.out}.
-
-A basic example is the native-code version of \Coq\ ({\tt coqtop.opt}),
-which can be generated by {\tt coqmktop -opt -o coqopt.opt}.
-
-
-\paragraph[Application: how to use the Objective Caml debugger with Coq.]{Application: how to use the Objective Caml debugger with Coq.\index{Debugger}}
-
-One useful application of \texttt{coqmktop} is to build a \Coq\ toplevel in
-order to debug your tactics with the Objective Caml debugger.
-You need to have configured and compiled \Coq\ for debugging
-(see the file \texttt{INSTALL} included in the distribution).
-Then, you must compile the Caml modules of your tactic with the
-option \texttt{-g} (with the bytecode compiler) and build a stand-alone
-bytecode toplevel with the following command:
-
-\begin{quotation}
-\texttt{\% coqmktop -g -o coq-debug}~\emph{<your \texttt{.cmo} files>}
-\end{quotation}
-
-
-To launch the \ocaml\ debugger with the image you need to execute it in
-an environment which correctly sets the \texttt{COQLIB} variable.
-Moreover, you have to indicate the directories in which
-\texttt{ocamldebug} should search for Caml modules.
-
-A possible solution is to use a wrapper around \texttt{ocamldebug}
-which detects the executables containing the word \texttt{coq}. In
-this case, the debugger is called with the required additional
-arguments. In other cases, the debugger is simply called without additional
-arguments. Such a wrapper can be found in the \texttt{dev/}
-subdirectory of the sources. 
-
-\section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
-  \index{Coqdep@{\tt coqdep}}}
-
-In order to compute modules dependencies (so to use {\tt make}),
-\Coq\ comes with an appropriate tool, {\tt coqdep}.
-
-{\tt coqdep} computes inter-module dependencies for \Coq\ and
-\ocaml\ programs, and prints the dependencies on the standard
-output in a format readable by make.  When a directory is given as
-argument, it is recursively looked at.
-
-Dependencies of \Coq\ modules are computed by looking at {\tt Require}
-commands ({\tt Require}, {\tt Requi\-re Export}, {\tt Require Import},
-but also at the command {\tt Declare ML Module}.
-
-Dependencies of \ocaml\ modules are computed by looking at
-\verb!open! commands and the dot notation {\em module.value}. However,
-this is done approximatively and you are advised to use {\tt ocamldep}
-instead for the \ocaml\ modules dependencies.
-
-See the man page of {\tt coqdep} for more details and options.
-
-
-\section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile}
-\index{Makefile@{\tt Makefile}}
-\index{CoqMakefile@{\tt coq\_Makefile}}}
-
-When a proof development becomes large, is split into several files or contains
-Ocaml plugins, it becomes crucial to use a tool like {\tt make} to compile
-\Coq\ modules.
-
-The writing of a generic and complete {\tt Makefile} may be a tedious work
-and that's why \Coq\ provides a tool to automate its creation,
-{\tt coq\_makefile}.
-
-You can get a description of the arguments by the command \texttt{\% coq\_makefile
-  --help}.  Arguments can be directly written on the command line interface but it is recommended
-to write them in a file ({\tt \_CoqProject} by default) and then call {\tt
-  coq\_makefile -f \_CoqProject -o Makefile}. That means options are read from {\tt
-  \_CoqProject} and written in {\tt Makefile}. This way, {\tt Makefile} will be
-automagically regenerated when something changes in {\tt \_CoqProject}.
-
-The first time you use this tool, you may be happy with:
-\begin{quotation}
-\texttt{\% \{ echo '-R .} {\em MyFancyLib} \texttt{' ; find -name '*.v' -print \} >
-  \_CoqProject \&\& coq\_makefile -f \_CoqProject -o Makefile}
-\end{quotation}
-
-To customize things further, remember the following:
-\begin{itemize}
-\item \Coq files must end in {\tt .v}, \ocaml modules in {\tt .ml4} if they
-  require camlp preproccessing (and in {\tt .ml} otherwise), and \ocaml module
-  signatures in {\tt .mli}.
-\item Whenever a directory is passed as argument, any inner {\tt Makefile} will be
-  recursively called.
-\item {\tt -R} option is for \Coq, {\tt -I} for \ocaml. The same directory can be
-  ``included'' by both.
-
-  Using {\tt -R} option gives a correct logical path and a correct installation
-  emplacement to your coq files.
-\item If your files depend on an external library, never use {\tt -R \dots} to
-  include it in the path, the {\em make clean} command would erase it! Take
-  advantage of the \verb:COQPATH: variable (see \ref{envars}) instead if
-  necessary.
-\end{itemize}
-
-Under normal circumstances, the only other variable that you may use is
-\verb:$COQBIN: to specify the directory where the binaries are.
-
-\section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
-\index{Coqdoc@{\sf coqdoc}}}
-
-\input{./coqdoc}
-
-\section{Exporting \Coq\ theories to XML}
-
-\input{./Helm}
-
-\section[Embedded \Coq\ phrases inside \LaTeX\ documents]{Embedded \Coq\ phrases inside \LaTeX\ documents\label{Latex}
-  \index{Coqtex@{\tt coq-tex}}\index{Latex@{\LaTeX}}}
-
-When writing a documentation about a proof development, one may want
-to insert \Coq\ phrases inside a \LaTeX\ document, possibly together with
-the corresponding answers of the system. We provide a
-mechanical way to process such \Coq\ phrases embedded in \LaTeX\ files: the
-{\tt coq-tex} filter.  This filter extracts Coq phrases embedded in
-LaTeX files, evaluates them, and insert the outcome of the evaluation
-after each phrase.
-
-Starting with a file {\em file}{\tt.tex} containing \Coq\ phrases,
-the {\tt coq-tex} filter produces a file named {\em file}{\tt.v.tex} with
-the \Coq\ outcome.
-
-There are options to produce the \Coq\ parts in smaller font, italic,
-between horizontal rules, etc.
-See the man page of {\tt coq-tex} for more details.
-
-\medskip\noindent {\bf Remark.} This Reference Manual and the Tutorial
-have been completely produced with {\tt coq-tex}.
-
-
-\section[\Coq\ and \emacs]{\Coq\ and \emacs\label{Emacs}\index{Emacs}}
-
-\subsection{The \Coq\ Emacs mode}
-
-\Coq\ comes with a Major mode for \emacs, {\tt coq.el}. This mode provides
-syntax highlighting
-and also a rudimentary indentation facility
-in the style of the Caml \emacs\ mode.
-
-Add the following lines to your \verb!.emacs! file:
-
-\begin{verbatim}
-  (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
-  (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)
-\end{verbatim}
-
-The \Coq\ major mode is triggered by visiting a file with extension {\tt .v},
-or manually with the command \verb!M-x coq-mode!.
-It gives you the correct syntax table for
-the \Coq\ language, and also a rudimentary indentation facility:
-\begin{itemize}
-  \item pressing {\sc Tab} at the beginning of a line indents the line like
-    the line above;
-
-  \item extra {\sc Tab}s increase the indentation level
-    (by 2 spaces by default);
-
-  \item M-{\sc Tab} decreases the indentation level.
-\end{itemize}
-
-An inferior mode to run \Coq\ under Emacs, by Marco Maggesi, is also
-included in the distribution, in file \texttt{coq-inferior.el}.
-Instructions to use it are contained in this file.
-
-\subsection[Proof General]{Proof General\index{Proof General}}
-
-Proof General is a generic interface for proof assistants based on
-Emacs. The main idea is that the \Coq\ commands you are
-editing are sent to a \Coq\ toplevel running behind Emacs and the
-answers of the system automatically inserted into other Emacs buffers. 
-Thus you don't need to copy-paste the \Coq\ material from your files
-to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
-files. 
-
-Proof General is developped and distributed independently of the
-system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
-
-
-\section[Module specification]{Module specification\label{gallina}\index{Gallina@{\tt gallina}}}
-
-Given a \Coq\ vernacular file, the {\tt gallina} filter extracts its
-specification (inductive types declarations, definitions, type of
-lemmas and theorems), removing the proofs parts of the file. The \Coq\
-file {\em file}{\tt.v} gives birth to the specification file
-{\em file}{\tt.g} (where the suffix {\tt.g} stands for \gallina).
-
-See the man page of {\tt gallina} for more details and options.
-
-
-\section[Man pages]{Man pages\label{ManPages}\index{Man pages}}
-
-There are man pages for the commands {\tt coqdep}, {\tt gallina} and
-{\tt coq-tex}. Man pages are installed at installation time
-(see installation instructions in file {\tt INSTALL}, step 6).
-
-%BEGIN LATEX
-\RefManCutCommand{ENDREFMAN=\thepage}
-%END LATEX
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: