"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

1 files changed, 49 insertions, 0 deletions

diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro
new file mode 100644
index 0000000000..3c0e262d47
--- /dev/null
+++ b/dev/ocamldoc/docintro
@@ -0,0 +1,49 @@
+{!indexlist}
+
+This is Coq, a proof assistant for the Calculus of Inductive Constructions.
+This document describes the implementation of Coq.
+It has been automatically generated from the source of
+Coq using {{:http://caml.inria.fr/}ocamldoc}.
+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 Constructions.}
+{- 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 constr_expr 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.}
+}