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, 25 insertions, 22 deletions

diff --git a/lib/rtree.mli b/lib/rtree.mli
index de5a9aa38..6dd66d104 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -1,24 +1,24 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(* Type of regular tree with nodes labelled by values of type 'a *)
-(* The implementation uses de Bruijn indices, so binding capture
+(** Type of regular tree with nodes labelled by values of type 'a 
+   The implementation uses de Bruijn indices, so binding capture
    is avoided by the lift operator (see example below) *)
 type 'a t
 
-(* Building trees *)
+(** Building trees *)
 
-(* build a node given a label and the vector of sons *)
+(** build a node given a label and the vector of sons *)
 val mk_node  : 'a -> 'a t array -> 'a t
 
-(* Build mutually recursive trees:
+(** Build mutually recursive trees:
     X_1 = f_1(X_1,..,X_n) ... X_n = f_n(X_1,..,X_n)
    is obtained by the following pseudo-code
    let vx = mk_rec_calls n in
@@ -32,27 +32,29 @@ val mk_node  : 'a -> 'a t array -> 'a t
   Another example: nested recursive trees rec Y = b(rec X = a(X,Y),Y,Y)
   let [|vy|] = mk_rec_calls 1 in
   let [|vx|] = mk_rec_calls 1 in
-  let [|x|] = mk_rec[|mk_node a [|vx;lift 1 vy|]
-  let [|y|] = mk_rec[|mk_node b [|x;vy;vy|]|]
+  let [|x|] = mk_rec[|mk_node a vx;lift 1 vy|]
+  let [|y|] = mk_rec[|mk_node b x;vy;vy|]
   (note the lift to avoid
  *)
 val mk_rec_calls : int -> 'a t array
 val mk_rec   : 'a t array -> 'a t array
 
-(* [lift k t] increases of [k] the free parameters of [t]. Needed
+(** [lift k t] increases of [k] the free parameters of [t]. Needed
    to avoid captures when a tree appears under [mk_rec] *)
 val lift : int -> 'a t -> 'a t
 
 val is_node : 'a t -> bool
-(* Destructors (recursive calls are expanded) *)
+
+(** Destructors (recursive calls are expanded) *)
 val dest_node  : 'a t -> 'a * 'a t array
-(* dest_param is not needed for closed trees (i.e. with no free variable) *)
+
+(** dest_param is not needed for closed trees (i.e. with no free variable) *)
 val dest_param : 'a t -> int * int
 
-(* Tells if a tree has an infinite branch *)
+(** Tells if a tree has an infinite branch *)
 val is_infinite : 'a t -> bool
 
-(* [compare_rtree f t1 t2] compares t1 t2 (top-down).
+(** [compare_rtree f t1 t2] compares t1 t2 (top-down).
    f is called on each node: if the result is negative then the
    traversal ends on false, it is is positive then deeper nodes are
    not examined, and the traversal continues on respective siblings,
@@ -66,14 +68,15 @@ val compare_rtree : ('a t -> 'b t -> int) -> 'a t -> 'b t -> bool
 
 val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 
-(* Iterators *)
+(** Iterators *)
 
 val map : ('a -> 'b) -> 'a t -> 'b t
-(* [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
+
+(** [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
 val smartmap : ('a -> 'a) -> 'a t -> 'a t
 val fold : (bool -> 'a t -> ('a t -> 'b) -> 'b) -> 'a t -> 'b
 val fold2 :
   (bool -> 'a t -> 'b -> ('a t -> 'b -> 'c) -> 'c) -> 'a t -> 'b -> 'c
 
-(* A rather simple minded pretty-printer *)
+(** A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds