From f73d7c4614d000f068550b5144d80b7eceed58e9 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 29 Apr 2010 09:56:37 +0000
Subject: Move from ocamlweb to ocamdoc to generate mli documentation

dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.

In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.

ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html

The possibility to put graphs in pdf/html seems to be lost.

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

(limited to 'dev/docintro')

diff --git a/dev/docintro b/dev/docintro
new file mode 100644
index 0000000000..3d37d5374d
--- /dev/null
+++ b/dev/docintro
@@ -0,0 +1,50 @@
+{!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