From e24d8149c3aefd11b03458b6f9b3e38ca454b07a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 May 2006 21:51:59 +0000
Subject: Restructuration dossier dev et mise à jour de certaines
 documentations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/intro.tex | 25 -------------------------
 1 file changed, 25 deletions(-)
 delete mode 100644 dev/doc/intro.tex

(limited to 'dev/doc/intro.tex')

diff --git a/dev/doc/intro.tex b/dev/doc/intro.tex
deleted file mode 100644
index 4cec8673f4..0000000000
--- a/dev/doc/intro.tex
+++ /dev/null
@@ -1,25 +0,0 @@
-
-\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
-- 
cgit v1.2.3