diff options
author | 2006-04-28 14:59:16 +0000 | |
---|---|---|
committer | 2006-04-28 14:59:16 +0000 | |
commit | 2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch) | |
tree | e1542c8adb83ff297284eefc23a2703461713d9b /dev/doc/intro.tex | |
parent | 514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff) | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'dev/doc/intro.tex')
-rw-r--r-- | dev/doc/intro.tex | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/dev/doc/intro.tex b/dev/doc/intro.tex new file mode 100644 index 00000000..4cec8673 --- /dev/null +++ b/dev/doc/intro.tex @@ -0,0 +1,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}
\ No newline at end of file |