blob: 4cec8673f4330048e42feb766e9aeb4db5130c49 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
\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}
|
