2
\ocwsection This is \Coq, a proof assistant for the \CCI.
3
This document describes the implementation of \Coq.
4
It has been automatically generated from the source of
5
\Coq\ using \textsf{ocamlweb}, a literate programming tool for
6
\textsf{Objective Caml}\footnote{\Coq, \textsf{Objective Caml} and
7
\textsf{ocamlweb} are all freely available at
8
\textsf{http://coq.inria.fr/}, \textsf{http://caml.inria.fr/} and
9
\textsf{http://www.lri.fr/\~{}filliatr/ocamlweb}.}.
10
The source files are organized in several directories, which are
11
described here as separate chapters.
14
\begin{tabular}{p{10cm}rr}
15
Chapter & section & page \\[0.5em]
17
Utility libraries \dotfill & \refsec{lib} & \pageref{lib} \\[0.5em]
18
Kernel \dotfill & \refsec{kernel} & \pageref{kernel} \\[0.5em]
19
Library \dotfill & \refsec{library} & \pageref{library} \\[0.5em]
20
Pretyping \dotfill & \refsec{pretyping} & \pageref{pretyping} \\[0.5em]
21
Proof engine \dotfill & \refsec{proofs} & \pageref{proofs} \\[0.5em]
22
Tactics \dotfill & \refsec{tactics} & \pageref{tactics} \\[0.5em]
23
Toplevel \dotfill & \refsec{toplevel}& \pageref{toplevel}\\[0.5em]
b'\\ No newline at end of file'