From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 doc/refman/coqdoc.tex | 480 --------------------------------------------------
 1 file changed, 480 deletions(-)
 delete mode 100644 doc/refman/coqdoc.tex

(limited to 'doc/refman/coqdoc.tex')

diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
deleted file mode 100644
index f2630da0..00000000
--- a/doc/refman/coqdoc.tex
+++ /dev/null
@@ -1,480 +0,0 @@
-
-%\newcommand{\Coq}{\textsf{Coq}}
-\newcommand{\javadoc}{\textsf{javadoc}}
-\newcommand{\ocamldoc}{\textsf{ocamldoc}}
-\newcommand{\coqdoc}{\textsf{coqdoc}}
-\newcommand{\texmacs}{\TeX{}macs}
-\newcommand{\monurl}[1]{#1}
-%HEVEA\renewcommand{\monurl}[1]{\ahref{#1}{#1}}
-%HEVEA\newcommand{\lnot}{not}
-%HEVEA\newcommand{\lor}{or}
-%HEVEA\newcommand{\land}{\&}
-%%% attention : -- dans un argument de \texttt est affiché comme un
-%%% seul - d'où l'utilisation de la macro suivante
-\newcommand{\mm}{\symbol{45}\symbol{45}}
-
-
-\coqdoc\ is a documentation tool for the proof assistant
-\Coq, similar to \javadoc\ or \ocamldoc. 
-The task of \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}
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\subsection{Principles}
-
-Documentation is inserted into \Coq\ files as \emph{special comments}.  
-Thus your files will compile as usual, whether you use \coqdoc\ or not.
-\coqdoc\ presupposes that the given \Coq\ files are well-formed (at
-least lexically).  Documentation starts with
-\texttt{(**}, followed by a space, and ends with the pending \texttt{*)}. 
-The documentation format is inspired
-  by Todd~A.~Coram's \emph{Almost Free Text (AFT)} tool: it is mainly
-ASCII text with some syntax-light controls, described below.
-\coqdoc\ is robust: it shouldn't fail, whatever the input is. But
-remember: ``garbage in, garbage out''.
-
-\paragraph{\Coq\ material inside documentation.}
-\Coq\ material is quoted between the
-delimiters \texttt{[} and \texttt{]}. Square brackets may be nested,
-the inner ones being understood as being part of the quoted code (thus
-you can quote a term like $[x:T]u$ by writing
-\texttt{[[x:T]u]}). Inside quotations, the code is pretty-printed in
-the same way as it is in code parts.
-
-Pre-formatted vernacular is enclosed by \texttt{[[} and
-\texttt{]]}. The former must be followed by a newline and the latter
-must follow a newline.
-
-\paragraph{Pretty-printing.}
-\coqdoc\ uses different faces for identifiers and keywords.  
-The pretty-printing of \Coq\ tokens (identifiers or symbols) can be
-controlled using one of the following commands:
-\begin{alltt}
-(** printing \emph{token} %...\LaTeX...% #...HTML...# *)
-\end{alltt}
-or
-\begin{alltt}
-(** printing \emph{token} $...\LaTeX\ math...$ #...HTML...# *)
-\end{alltt}
-It gives the \LaTeX\ and HTML texts to be produced for the given \Coq\
-token. One of the \LaTeX\ or HTML text may be ommitted, causing the
-default pretty-printing to be used for this token.
-
-The printing for one token can be removed with
-\begin{alltt}
-(** remove printing \emph{token} *)
-\end{alltt}
-
-Initially, the pretty-printing table contains the following mapping:
-\begin{center}
-  \begin{tabular}{ll@{\qquad\qquad}ll@{\qquad\qquad}ll@{\qquad\qquad}}
-    \verb!->!            & $\rightarrow$   &
-    \verb!<-!            & $\leftarrow$    &
-    \verb|*|             & $\times$        \\
-    \verb|<=|            & $\le$           &
-    \verb|>=|            & $\ge$           &
-    \verb|=>|            & $\Rightarrow$   \\
-    \verb|<>|            & $\not=$         &
-    \verb|<->|           & $\leftrightarrow$ &
-    \verb!|-!            & $\vdash$        \\
-    \verb|\/|            & $\lor$          &
-    \verb|/\|            & $\land$         &
-    \verb|~|             & $\lnot$ 
-  \end{tabular}
-\end{center}
-Any of these can be overwritten or suppressed using the
-\texttt{printing} commands.
-
-Important note: the recognition of tokens is done by a (ocaml)lex
-automaton and thus applies the longest-match rule. For instance,
-\verb!->~! is recognized as a single token, where \Coq\ sees two
-tokens. It is the responsability of the user to insert space between
-tokens \emph{or} to give pretty-printing rules for the possible
-combinations, e.g. 
-\begin{verbatim}
-(** printing ->~ %\ensuremath{\rightarrow\lnot}% *)
-\end{verbatim}
-
-
-\paragraph{Sections.}
-Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the
-line). One star is a section, two stars a sub-section, etc.
-The section title is given on the remaining of the line.
-Example:
-\begin{verbatim}
-    (** * Well-founded relations
-  
-        In this section, we introduce...  *)
-\end{verbatim}
-
-
-%TODO \paragraph{Fonts.}
-
-
-\paragraph{Lists.}
-List items are introduced by 1 to 4 leading dashes.
-Deepness of the list is indicated by the number of dashes.
-List ends with a blank line.
-Example:
-\begin{verbatim}
-    This module defines
-        - the predecessor [pred]
-        - the addition [plus]
-        - order relations:
-          -- less or equal [le]
-          -- less [lt]
-\end{verbatim}
-
-\paragraph{Rules.}
-More than 4 leading dashes produce an horizontal rule.
-
-
-\paragraph{Escapings to \LaTeX\ and HTML.}
-Pure \LaTeX\ or HTML material can be inserted using the following
-escape sequences:
-\begin{itemize}
-\item \verb+$...LaTeX stuff...$+ inserts some \LaTeX\ material in math mode.
-  Simply discarded in HTML output.
-
-\item \verb+%...LaTeX stuff...%+ inserts some \LaTeX\ material.
-  Simply discarded in HTML output.
-
-\item \verb+#...HTML stuff...#+ inserts some HTML material. Simply
-  discarded in \LaTeX\ output.
-\end{itemize}
-
-
-\paragraph{Verbatim.} 
-Verbatim material is introduced by a leading \verb+<<+ and closed by
-\verb+>>+. Example:
-\begin{verbatim}
-Here is the corresponding caml code:
-<<
-  let rec fact n = 
-    if n <= 1 then 1 else n * fact (n-1)
->>
-\end{verbatim}
-
-
-\paragraph{Hyperlinks.}
-Hyperlinks can be inserted into the HTML output, so that any
-identifier is linked to the place of its definition.
-
-In order to get hyperlinks you need to first compile your \Coq\ file
-using \texttt{coqc \mm{}dump-glob \emph{file}}; this appends 
-\Coq\ names resolutions done during the compilation to file
-\texttt{\emph{file}}. Take care of erasing this file, if any, when
-starting the whole compilation process.
-
-Then invoke \texttt{coqdoc \mm{}glob-from \emph{file}} to tell
-\coqdoc\ to look for name resolutions into the file \texttt{\emph{file}}.
-
-Identifiers from the \Coq\ standard library are linked to the \Coq\
-web site at \url{http://coq.inria.fr/library/}. This behavior can be
-changed using command line options \url{--no-externals} and
-\url{--coqlib}; see below.
-
-
-\paragraph{Hiding / Showing parts of the source.}
-Some parts of the source can be hidden using command line options
-\texttt{-g} and \texttt{-l} (see below), or using such comments:
-\begin{alltt}
-(* begin hide *)
-\emph{some Coq material}
-(* end hide *)
-\end{alltt}
-Conversely, some parts of the source which would be hidden can be
-shown using such comments: 
-\begin{alltt}
-(* begin show *)
-\emph{some Coq material}
-(* end show *)
-\end{alltt}
-The latter cannot be used around some inner parts of a proof, but can
-be used around a whole proof.
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\subsection{Usage}
-
-\coqdoc\ is invoked on a shell command line as follows:
-\begin{displaymath}
-  \texttt{coqdoc }<\textit{options and files}>
-\end{displaymath}
-Any command line argument which is not an option is considered to be a
-file (even if it starts with a \verb!-!). \Coq\ files are identified
-by the suffixes \verb!.v! and \verb!.g! and \LaTeX\ files by the
-suffix \verb!.tex!. 
-
-\begin{description}
-\item[HTML output] ~\par
-  This is the default output.
-  One HTML file is created for each \Coq\ file given on the command line,
-  together with a file \texttt{index.html} (unless option
-  \texttt{-no-index} is passed). The HTML pages use a style sheet
-  named \texttt{style.css}. Such a file is distributed with \coqdoc.
-
-\item[\LaTeX\ output] ~\par
-  A single \LaTeX\ file is created, on standard output. It can be
-  redirected to a file with option \texttt{-o}. 
-  The order of files on the command line is kept in the final
-  document. \LaTeX\ files given on the command line are copied `as is'
-  in the final document .
-  DVI and PostScript can be produced directly with the options
-  \texttt{-dvi} and \texttt{-ps} respectively.
-
-\item[\texmacs\ output] ~\par
-  To translate the input files to \texmacs\ format, to be used by
-  the \texmacs\ Coq interface 
-  (see \url{http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/}).
-\end{description}
-
-
-\subsubsection*{Command line options}
-
-
-\paragraph{Overall options}
-
-\begin{description}
-
-\item[\texttt{\mm{}html}] ~\par
-  
-  Select a HTML output.
-
-\item[\texttt{\mm{}latex}] ~\par
-  
-  Select a \LaTeX\ output.
-
-\item[\texttt{\mm{}dvi}] ~\par
-  
-  Select a DVI output.
-
-\item[\texttt{\mm{}ps}] ~\par
-  
-  Select a PostScript output.
-
-\item[\texttt{\mm{}texmacs}] ~\par
-  
-  Select a \texmacs\ output.
-
-\item[\texttt{--stdout}] ~\par
-
-  Write output to stdout.
-
-\item[\texttt{-o }\textit{file}, \texttt{\mm{}output }\textit{file}] ~\par
-  
-  Redirect the output into the file `\textit{file}' (meaningless with
-  \texttt{-html}).
-
-\item[\texttt{-d }\textit{dir}, \texttt{\mm{}directory }\textit{dir}] ~\par
-
-  Output files into directory `\textit{dir}' instead of current
-  directory (option \texttt{-d} does not change the filename specified
-  with option \texttt{-o}, if any).
-
-\item[\texttt{-s }, \texttt{\mm{}short}] ~\par
-  
-  Do not insert titles for the files. The default behavior is to
-  insert a title like ``Library Foo'' for each file.
-
-\item[\texttt{-t }\textit{string}, 
-      \texttt{\mm{}title }\textit{string}] ~\par
-  
-  Set the document title.      
-
-\item[\texttt{\mm{}body-only}] ~\par
-
-  Suppress the header and trailer of the final document. Thus, you can
-  insert the resulting document into a larger one.
-
-\item[\texttt{-p} \textit{string}, \texttt{\mm{}preamble} \textit{string}]~\par
-
-  Insert some material in the \LaTeX\ preamble, right before
-  \verb!\begin{document}! (meaningless with \texttt{-html}).
-
-\item[\texttt{\mm{}vernac-file }\textit{file},
-      \texttt{\mm{}tex-file }\textit{file}] ~\par
-      
-      Considers the file `\textit{file}' respectively as a \verb!.v!
-      (or \verb!.g!) file or a \verb!.tex! file.
-
-\item[\texttt{\mm{}files-from }\textit{file}] ~\par
-
-  Read file names to process in file `\textit{file}' as if they were
-  given on the command line. Useful for program sources splitted in
-  several directories.
-  
-\item[\texttt{-q}, \texttt{\mm{}quiet}] ~\par
-
-  Be quiet. Do not print anything except errors.
-
-\item[\texttt{-h}, \texttt{\mm{}help}] ~\par
-
-  Give a short summary of the options and exit.
-
-\item[\texttt{-v}, \texttt{\mm{}version}] ~\par
-
-  Print the version and exit.
-
-\end{description}
-
-\paragraph{Index options} ~\par
-
-Default behavior is to build an index, for the HTML output only, into
-\texttt{index.html}.
-
-\begin{description}
-
-\item[\texttt{\mm{}no-index}] ~\par
-  
-  Do not output the index.
-
-\item[\texttt{\mm{}multi-index}] ~\par
-  
-  Generate one page for each category and each letter in the index,
-  together with a top page \texttt{index.html}.
-
-\end{description}
-
-\paragraph{Table of contents option} ~\par
-
-\begin{description}
-
-\item[\texttt{-toc}, \texttt{\mm{}table-of-contents}] ~\par
-
-  Insert a table of contents.
-  For a \LaTeX\ output, it inserts a \verb!\tableofcontents! at the
-  beginning of the document. For a HTML output, it builds a table of
-  contents into \texttt{toc.html}.
-
-\end{description}
-
-\paragraph{Hyperlinks options}
-\begin{description}
-
-\item[\texttt{\mm{}glob-from }\textit{file}] ~\par
-  
-  Make references using \Coq\ globalizations from file \textit{file}. 
-  (Such globalizations are obtained with \Coq\ option \texttt{-dump-glob}).
-
-\item[\texttt{\mm{}no-externals}] ~\par
-  
-  Do not insert links to the \Coq\ standard library.
-
-\item[\texttt{\mm{}coqlib }\textit{url}] ~\par
-
-  Set base URL for the \Coq\ standard library (default is 
-  \url{http://coq.inria.fr/library/}).
-
-\item[\texttt{-R }\textit{dir }\textit{coqdir}] ~\par
-
-  Map physical directory \textit{dir} to \Coq\ logical directory
-  \textit{coqdir} (similarly to \Coq\ option \texttt{-R}).
-
-  Note: option \texttt{-R} only has effect on the files
-  \emph{following} it on the command line, so you will probably need
-  to put this option first.
-
-\end{description}
-
-\paragraph{Contents options}
-\begin{description}
-
-\item[\texttt{-g}, \texttt{\mm{}gallina}] ~\par
-
-  Do not print proofs.
-
-\item[\texttt{-l}, \texttt{\mm{}light}] ~\par
-  
-  Light mode. Suppress proofs (as with \texttt{-g}) and the following commands:
-  \begin{itemize}
-  \item {}[\texttt{Recursive}] \texttt{Tactic Definition}
-  \item \texttt{Hint / Hints} 
-  \item \texttt{Require}
-  \item \texttt{Transparent / Opaque}
-  \item \texttt{Implicit Argument / Implicits}
-  \item \texttt{Section / Variable / Hypothesis / End}
-  \end{itemize}
-
-\end{description}
-The behavior of options \texttt{-g} and \texttt{-l} can be locally
-overridden using the \texttt{(* begin show *)} \dots\ \texttt{(* end
-  show *)} environment (see above).
-
-\paragraph{Language options} ~\par
-
-Default behavior is to assume ASCII 7 bits input files.
-
-\begin{description}
-
-\item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par
-
-  Select ISO-8859-1 input files. It is equivalent to
-  \texttt{--inputenc latin1 --charset iso-8859-1}.
-
-\item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par
-
-  Select UTF-8 (Unicode) input files. It is equivalent to
-  \texttt{--inputenc utf8 --charset utf-8}.
-  \LaTeX\ UTF-8 support can be found at
- \url{http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/}.
-
-\item[\texttt{\mm{}inputenc} \textit{string}] ~\par
-
-  Give a \LaTeX\ input encoding, as an option to \LaTeX\ package
-  \texttt{inputenc}. 
-
-\item[\texttt{\mm{}charset} \textit{string}] ~\par
-
-  Specify the HTML character set, to be inserted in the HTML header.
-
-\end{description}
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-\subsection{The coqdoc \LaTeX{} style file}
-\label{section:coqdoc.sty}
-
-In case you choose to produce a document without the default \LaTeX{}
-preamble (by using option \verb|--no-preamble|), then you must insert
-into your own preamble the command
-\begin{quote}
-  \verb|\usepackage{coqdoc}|
-\end{quote}
-Then you may alter the rendering of the document by
-redefining some macros:
-\begin{description}
-
-\item[\texttt{coqdockw}, \texttt{coqdocid}] ~ 
-  
-  The one-argument macros for typesetting keywords and identifiers.
-  Defaults are sans-serif for keywords and italic for identifiers.
-
-  For example, if you would like a slanted font for keywords, you
-  may insert  
-\begin{verbatim}
-     \renewcommand{\coqdockw}[1]{\textsl{#1}}
-\end{verbatim}
-  anywhere between \verb|\usepackage{coqdoc}| and
-  \verb|\begin{document}|. 
-
-\item[\texttt{coqdocmodule}] ~ 
-  
-  One-argument macro for typesetting the title of a \verb|.v| file.
-  Default is
-\begin{verbatim}
-\newcommand{\coqdocmodule}[1]{\section*{Module #1}}
-\end{verbatim}
-  and you may redefine it using \verb|\renewcommand|.
-
-\end{description}
-
-
-- 
cgit v1.2.3

