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, 19 insertions, 19 deletions

diff --git a/lib/heap.mli b/lib/heap.mli
index 777e356de7..a8c70d37d2 100644
--- a/lib/heap.mli
+++ b/lib/heap.mli
@@ -1,14 +1,14 @@
-(************************************************************************)
-(*  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*)
 
-(* Heaps *)
+(** Heaps *)
 
 module type Ordered = sig
   type t
@@ -17,29 +17,29 @@ end
 
 module type S =sig
 
-  (* Type of functional heaps *)
+  (** Type of functional heaps *)
   type t
 
-  (* Type of elements *)
+  (** Type of elements *)
   type elt
 
-  (* The empty heap *)
+  (** The empty heap *)
   val empty : t
 
-  (* [add x h] returns a new heap containing the elements of [h], plus [x];
-     complexity $O(log(n))$ *)
+  (** [add x h] returns a new heap containing the elements of [h], plus [x];
+     complexity {% $ %}O(log(n)){% $ %} *)
   val add : elt -> t -> t
 
-  (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
-     when [h] is empty; complexity $O(1)$ *)
+  (** [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
+     when [h] is empty; complexity {% $ %}O(1){% $ %} *)
   val maximum : t -> elt
 
-  (* [remove h] returns a new heap containing the elements of [h], except
+  (** [remove h] returns a new heap containing the elements of [h], except
      the maximum of [h]; raises [EmptyHeap] when [h] is empty;
-     complexity $O(log(n))$ *)
+     complexity {% $ %}O(log(n)){% $ %} *)
   val remove : t -> t
 
-  (* usual iterators and combinators; elements are presented in
+  (** usual iterators and combinators; elements are presented in
      arbitrary order *)
   val iter : (elt -> unit) -> t -> unit
 
@@ -49,6 +49,6 @@ end
 
 exception EmptyHeap
 
-(*S Functional implementation. *)
+(** {6 Functional implementation. } *)
 
 module Functional(X: Ordered) : S with type elt=X.t