diff options
| -rwxr-xr-x | doc/RefMan-uti.tex | 35 |
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} |