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

1 files changed, 0 insertions, 47 deletions

diff --git a/dev/ocamlweb-doc/ast.ml b/dev/ocamlweb-doc/ast.ml
deleted file mode 100644
index 4eb135d83..000000000
--- a/dev/ocamlweb-doc/ast.ml
+++ /dev/null
@@ -1,47 +0,0 @@
-
-type constr_ast =
-  Pair of constr_ast * constr_ast
-| Prod of binder list * constr_ast
-| Lambda of binder list * constr_ast
-| Let of string * constr_ast * constr_ast
-| LetCase of binder list * constr_ast * constr_ast
-| IfCase of constr_ast * constr_ast * constr_ast
-| Eval of red_fun * constr_ast
-| Infix of string * constr_ast * constr_ast
-| Prefix of string * constr_ast
-| Postfix of string * constr_ast
-| Appl of constr_ast * constr_arg list
-| ApplExpl of string list * constr_ast list
-| Scope of string * constr_ast
-| Qualid of string list
-| Prop | Set | Type
-| Int of string
-| Hole
-| Meta of string
-| Fixp of fix_kind *
-      (string * binder list * constr_ast * string option * constr_ast) list *
-      string
-| Match of case_item list * constr_ast option *
-           (pattern list * constr_ast) list
-
-and red_fun = Simpl
-
-and binder = string * constr_ast
-
-and constr_arg = string option * constr_ast
-
-and fix_kind = Fix | CoFix
-
-and case_item = constr_ast * (string option * constr_ast option)
-
-and pattern =
-  PatAs of pattern * string
-| PatType of pattern * constr_ast
-| PatConstr of string * pattern list
-| PatVar of string
-
-let mk_cast c t =
-  if t=Hole then c else Infix(":",c,t)
-
-let mk_lambda bl t =
-  if bl=[] then t else Lambda(bl,t)