1 files changed, 29 insertions, 74 deletions
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 5f201b67..bda4cff9 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -84,85 +84,42 @@ 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:
+{\tt coq\_makefile}.
 
-\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:
+Arguments are explain by \texttt{\% coq\_makefile --help}.  They can be directly
+written in the command line but it is recommended to write them in a file (called
+for example {\tt Make}) and then call {\tt coq\_makefile -f Make -o
+  Makefile}. That means options are in {\tt Make} file and output is {\tt
+  Makefile} This way, {\tt Makefile} will be automatically regenerated if
+something changes in {\tt Make}.
 
+The first time you use this tool, you may be happy with:
 \begin{quotation}
-\texttt{\% make depend}
+\texttt{\% \{ echo '-R .} {\em MyFancyLib} \texttt{' ; find -name '*.v' -print \} >
+  Make \&\& coq\_makefile -f Make -o Makefile}
 \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}
+To customize things afterwards, remember:
+\begin{itemize}
+\item Coq files must end in {\tt .v}, caml modules in {\tt .ml4} if they
+  require camlp preproccessing (and in {\tt .ml} otherwise), and caml module signatures in {\tt
+    .mli}.
+\item If you give a directory directly as argument, it is because you provide a
+  Makefile for it in it.
+\item {\tt -R} option is for Coq, {\tt -I} for caml. The same directory can
+  ``included'' by both.
+  Using {\tt -R} option gives a right logical path and a correct installation
+  emplacement to your coq files.
+\item If your files depend on an external library that isn't install somewhere
+  looked by coqc, use {\tt OTHERFLAGS = '-R path/to/lib lib\_name'} option in your {\tt
+    Make} but don't do {\tt -R \dots} directly, the {\em make clean} command would
+  erase it!
+\end{itemize}
 
 \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}}}
 
@@ -200,8 +157,8 @@ have been completely produced with {\tt coq-tex}.
 \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
+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:
@@ -232,7 +189,7 @@ 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
+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
@@ -264,8 +221,6 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and
 \RefManCutCommand{ENDREFMAN=\thepage}
 %END LATEX
 
-% $Id: RefMan-uti.tex 11975 2009-03-14 11:29:36Z letouzey $
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: t