From 8e66761c81648add03ed21b157a3bace716b8e08 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 29 Apr 2010 16:33:36 +0000
Subject: "make source-doc" builds documentation of mli in html and pdf at
 dev/ocamldoc/

old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)

"make clean" cleans dev/ocamldoc/ properly

wierd? calls of dependency graph generation leave unchanged

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

(limited to 'dev/docintro')

diff --git a/dev/docintro b/dev/docintro
deleted file mode 100644
index 3d37d5374d..0000000000
--- a/dev/docintro
+++ /dev/null
@@ -1,50 +0,0 @@
-{!indexlist}
-
-This is Coq, a proof assistant for the Calculus of Inductive Construction.
-This document describes the implementation of Coq.
-It has been automatically generated from the source of
-Coq using ocamldoc, a literate programming tool for
-Objective Caml  freely available at http://caml.inria.fr/.
-The source files are organized in several directories ordered like that:
-
-{ol {- Utility libraries : lib
-
-describes the various utility libraries used in the code
-of Coq.}
-{- Kernel : kernel
-
-describes the \Coq\ kernel, which is a type checker for the Calculus
-of Inductive Construction.}
-{- Library : library
-
-describes the Coq library, which is made of two parts:
-- a general mechanism to keep a trace of all operations and of
-    the state of the system, with backtrack capabilities;
-- a global environment for the CCI, with functions to export and 
-    import compiled modules.
-
-}
-{- Pretyping : pretyping
-
-}
-{- Front abstract syntax of terms : interp
-
-describes the translation from Coq context-dependent
-front abstract syntax of terms {v front v} to and from the
-context-free, untyped, raw form of constructions {v rawconstr v}.}
-{- Parsers and printers : parsing
-
-describes the implementation of the \Coq\ parsers and printers.}
-{- Proof engine : proofs
-
-describes the Coq proof engine, which is also called
-the ``refiner'', since it provides a way to build terms by successive
-refining steps. Those steps are either primitive rules or higher-level
-tactics.}
-{- Tacticts : tactics
-
-describes the Coq main tactics.}
-{- Toplevel : toplevel
-
-describes the highest modules of the Coq system.}
-}
-- 
cgit v1.2.3