1 files changed, 0 insertions, 272 deletions
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
deleted file mode 100644
index 5f201b67..00000000
--- a/doc/refman/RefMan-uti.tex
+++ /dev/null
@@ -1,272 +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 and is split into several files,
-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}. Given the files to compile, the command {\tt
-coq\_makefile} prints a 
-{\tt Makefile} on the standard output. So one has just to run the
-command:
-
-\begin{quotation}
-\texttt{\% coq\_makefile} {\em file$_1$.v \dots\ file$_n$.v} \texttt{> Makefile}
-\end{quotation}
-
-The resulted {\tt Makefile} has a target {\tt depend} which computes the
-dependencies and puts them in a separate file {\tt .depend}, which is
-included by the {\tt Makefile}. 
-Therefore, you should create such a file before the first invocation
-of make. You can for instance use the command 
-
-\begin{quotation}
-\texttt{\% touch .depend}
-\end{quotation}
-
-Then, to initialize or update the modules dependencies, type in:
-
-\begin{quotation}
-\texttt{\% make depend}
-\end{quotation}
-
-There is a target {\tt all} to compile all the files {\em file$_1$
-\dots\ file$_n$}, and a generic target to produce a {\tt .vo} file from
-the corresponding {\tt .v} file (so you can do {\tt make} {\em file}{\tt.vo}
-to compile the file {\em file}{\tt.v}).
-
-{\tt coq\_makefile} can also handle the case of ML files and
-subdirectories. For more options type
-
-\begin{quotation}
-\texttt{\% coq\_makefile --help}
-\end{quotation}
-
-\Warning To compile a project containing \ocaml{} files you must keep
-the sources of \Coq{} somewhere and have an environment variable named
-\texttt{COQTOP} that points to that directory.
-
-% \section{{\sf Coq\_SearchIsos}: information retrieval in a \Coq\ proofs
-% library}
-% \label{coqsearchisos}
-% \index{Coq\_SearchIsos@{\sf Coq\_SearchIsos}}
-
-% In the \Coq\ distribution, there is also a separated and independent tool,
-% called {\sf Coq\_SearchIsos}, which allows the search in accordance with {\tt
-% SearchIsos}\index{SearchIsos@{\tt SearchIsos}} (see Section~\ref{searchisos})
-% in a \Coq\ proofs library. More precisely, this program begins, once launched
-% by {\tt coqtop -searchisos}\index{coqtopsearchisos@{\tt
-% coqtop -searchisos}}, loading lightly (by using specifications functions)
-% all the \Coq\ objects files ({\tt .vo}) accessible by the {\tt LoadPath} (see
-% Section~\ref{loadpath}). Next, a prompt appears and four commands are then
-% available:
-
-% \begin{description}
-% \item [{\tt SearchIsos}]\ \\
-%   Scans the fixed context.
-% \item [{\tt Time}]\index{Time@{\tt Time}}\ \\
-%   Turns on the Time Search Display mode (see Section~\ref{time}).
-% \item [{\tt Untime}]\index{Untime@{\tt Untime}}\ \\
-%   Turns off the Time Search Display mode (see Section~\ref{time}).
-% \item [{\tt Quit}]\index{Quit@{\tt Quit}}\ \\
-%   Ends the {\tt coqtop -searchisos} session.
-% \end{description}
-
-% When running {\tt coqtop -searchisos} you can use the two options:
-
-% \begin{description}
-% \item[{\tt -opt}]\ \\
-%   Runs the native-code version of {\sf Coq\_SearchIsos}.
-
-% \item[{\tt -image} {\em file}]\ \\
-%   This option sets the binary image to be used to be {\em file}
-%   instead of the standard one. Not of general use.
-% \end{description}
-
-
-\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 (assuming your \emacs\ library provides
-{\tt hilit19.el}) 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 (or XEmacs). 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
-
-% $Id: RefMan-uti.tex 11975 2009-03-14 11:29:36Z letouzey $
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: