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