\ocwsection This is \Coq, a proof assistant for the \CCI.
This document describes the implementation of \Coq.
It has been automatically generated from the source of
\Coq\ using \textsf{ocamlweb}, a literate programming tool for
\textsf{Objective Caml}\footnote{\Coq, \textsf{Objective Caml} and
  \textsf{ocamlweb} are all freely available at
  \textsf{http://coq.inria.fr/}, \textsf{http://caml.inria.fr/} and
  \textsf{http://www.lri.fr/\~{}filliatr/ocamlweb}.}.
The source files are organized in several directories, which are
described here as separate chapters.

\begin{center}
  \begin{tabular}{p{10cm}rr}
    Chapter & section & page \\[0.5em]
    \hline\\[0.2em]
    Utility libraries \dotfill & \refsec{lib}     & \pageref{lib}     \\[0.5em]
    Kernel            \dotfill & \refsec{kernel}  & \pageref{kernel}  \\[0.5em]
    Library           \dotfill & \refsec{library} & \pageref{library} \\[0.5em]
    Pretyping     \dotfill & \refsec{pretyping} & \pageref{pretyping} \\[0.5em]
    Proof engine      \dotfill & \refsec{proofs}  & \pageref{proofs}  \\[0.5em]
    Tactics           \dotfill & \refsec{tactics} & \pageref{tactics} \\[0.5em]
    Toplevel          \dotfill & \refsec{toplevel}& \pageref{toplevel}\\[0.5em]
  \end{tabular}
\end{center}