utilitaires

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

1 files changed, 14 insertions, 21 deletions

diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex
index 9d3f7b7610..0c594cfab3 100755
--- a/doc/RefMan-uti.tex
+++ b/doc/RefMan-uti.tex
@@ -192,28 +192,21 @@ See the man page of {\tt coq-tex} for more details.
 have been completely produced with {\tt coq-tex}.
 
 
-\subsection{Documenting \Coq\ files with \LaTeX}
-  \index{Coqweb@{\tt coqweb}}
-
-\verb!coqweb! is a ``literate programming'' tool for \Coq, inspired
-by Knuth's WEB tool. The user documents his or her files with \LaTeX\ material
-inside \Coq\ comments and \verb!coqweb! produces a \LaTeX\ document
-from this unique source.
-\Coq\ parts are displayed in a nice way (\verb!->! becomes
-$\rightarrow$, keywords are typeset in a bold face,
-etc.). Additionally, an index is produced which gives the places where
-the various globals are introduced.
-
-\verb!coqweb! is developped and distributed independently of the
+\subsection{Documenting \Coq\ files}
+  \index{Coqdoc@{\tt coqdoc}}
+
+A nice documentation can be produced from \Coq\ sources using the 
+documentation tool \verb!coqdoc!.
+The task of \verb!coqdoc! is
+\begin{enumerate}
+\item to produce a nice \LaTeX\ and/or HTML document from the Coq
+  sources, readable for a human and not only for the proof assistant; 
+\item to help the user navigating in his own (or third-party) sources. 
+\end{enumerate}
+
+\verb!coqdoc! is developped and distributed independently of the
 system \Coq. It is freely available, with sources, binaries and a full
-documentation, at \verb!www.lri.fr/~filliatr/coqweb!.
-
-
-\section{\Coq\ and HTML}\label{Html}\index{HTML}
-
-An HTML output can be obtained from \Coq\ files documented using
-\verb!coqweb! (see the previous paragraph). See the documentation of
-\verb!coqweb! for more details.
+documentation, at \verb!www.lri.fr/~filliatr/coqdoc/!.
 
 
 \section{\Coq\ and \emacs}\label{Emacs}\index{Emacs}