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

23 files changed, 335 insertions, 311 deletions

diff --git a/lib/bigint.mli b/lib/bigint.mli
index 69b035c45c..06f5422278 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -1,18 +1,16 @@
-(************************************************************************)
-(*  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*)
 
-(*i*)
 open Pp
-(*i*)
 
-(* Arbitrary large integer numbers *)
+(** Arbitrary large integer numbers *)
 
 type bigint
 
@@ -23,7 +21,7 @@ val zero : bigint
 val one : bigint
 val two : bigint
 
-val div2_with_rest : bigint -> bigint * bool (* true=odd; false=even *)
+val div2_with_rest : bigint -> bigint * bool (** true=odd; false=even *)
 val add_1 : bigint -> bigint
 val sub_1 : bigint -> bigint
 val mult_2 : bigint -> bigint
diff --git a/lib/dnet.mli b/lib/dnet.mli
index 61998d6301..8b50fae239 100644
--- a/lib/dnet.mli
+++ b/lib/dnet.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        
+  ***********************************************************************)
 
-(* $Id:$ *)
+(** {% $ %}Id:{% $ %} *)
 
-(* Generic discrimination net implementation over recursive
+(** Generic discrimination net implementation over recursive
    types. This module implements a association data structure similar
    to tries but working on any types (not just lists). It is a term
    indexing datastructure, a generalization of the discrimination nets
@@ -43,27 +43,27 @@
 
 *)
 
-(* datatype you want to build a dnet on *)
+(** datatype you want to build a dnet on *)
 module type Datatype =
 sig
-  (* parametric datatype. ['a] is morally the recursive argument *)
+  (** parametric datatype. ['a] is morally the recursive argument *)
   type 'a t
 
-  (* non-recursive mapping of subterms *)
+  (** non-recursive mapping of subterms *)
   val map : ('a -> 'b) -> 'a t -> 'b t
   val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
 
-  (* non-recursive folding of subterms *)
+  (** non-recursive folding of subterms *)
   val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
   val fold2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a
 
-  (* comparison of constructors *)
+  (** comparison of constructors *)
   val compare : unit t -> unit t -> int
 
-  (* for each constructor, is it not-parametric on 'a? *)
+  (** for each constructor, is it not-parametric on 'a? *)
   val terminal : 'a t -> bool
 
-  (* [choose f w] applies f on ONE of the subterms of w *)
+  (** [choose f w] applies f on ONE of the subterms of w *)
   val choose : ('a -> 'b) -> 'a t -> 'b
 end
 
@@ -71,19 +71,19 @@ module type S =
 sig
   type t
 
-  (* provided identifier type *)
+  (** provided identifier type *)
   type ident
 
-  (* provided metavariable type *)
+  (** provided metavariable type *)
   type meta
 
-  (* provided parametrized datastructure *)
+  (** provided parametrized datastructure *)
   type 'a structure
 
-  (* returned sets of solutions *)
+  (** returned sets of solutions *)
   module Idset : Set.S with type elt=ident
 
-  (* a pattern is a term where each node can be a unification
+  (** a pattern is a term where each node can be a unification
      variable *)
   type 'a pattern =
     | Term of 'a
@@ -93,13 +93,13 @@ sig
 
   val empty : t
 
-  (* [add t w i] adds a new association (w,i) in t. *)
+  (** [add t w i] adds a new association (w,i) in t. *)
   val add : t -> term_pattern -> ident -> t
 
-  (* [find_all t] returns all identifiers contained in t. *)
+  (** [find_all t] returns all identifiers contained in t. *)
   val find_all : t -> Idset.t
 
-  (* [fold_pattern f acc p dn] folds f on each meta of p, passing the
+  (** [fold_pattern f acc p dn] folds f on each meta of p, passing the
      meta and the sub-dnet under it. The result includes:
      - Some set if identifiers were gathered on the leafs of the term
      - None if the pattern contains no leaf (only Metas at the leafs).
@@ -107,15 +107,15 @@ sig
   val fold_pattern :
     ('a -> (Idset.t * meta * t) -> 'a) -> 'a -> term_pattern -> t -> Idset.t option * 'a
 
-  (* [find_match p t] returns identifiers of all terms matching p in
+  (** [find_match p t] returns identifiers of all terms matching p in
      t. *)
   val find_match : term_pattern -> t -> Idset.t
 
-  (* set operations on dnets *)
+  (** set operations on dnets *)
   val inter : t -> t -> t
   val union : t -> t -> t
 
-  (* apply a function on each identifier and node of terms in a dnet *)
+  (** apply a function on each identifier and node of terms in a dnet *)
   val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
 end
 
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 1149612f11..befc8de7e3 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.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*)
 
-(* Dynamics. Use with extreme care. Not for kids. *)
+(** Dynamics. Use with extreme care. Not for kids. *)
 
 type t
 
diff --git a/lib/envars.mli b/lib/envars.mli
index 62d0cb61d0..8e4ccb4d5d 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -1,10 +1,13 @@
-(************************************************************************)
-(*  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        
+  ***********************************************************************)
+
+(** This file gathers environment variables needed by Coq to run (such
+   as coqlib) *)
 
 val coqlib : unit -> string
 val coqbin : unit -> string
diff --git a/lib/explore.mli b/lib/explore.mli
index e29f27955a..34a472b72b 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -1,16 +1,17 @@
-(************************************************************************)
-(*  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*)
 
-(*s Search strategies. *)
+(** {6 Search strategies. } *)
 
-(*s A search problem implements the following signature [SearchProblem].
+(** {6 Sect } *)
+(** A search problem implements the following signature [SearchProblem].
     [state] is the type of states of the search tree.
     [branching] is the branching function; if [branching s] returns an
     empty list, then search from [s] is aborted; successors of [s] are
@@ -32,7 +33,8 @@ module type SearchProblem = sig
 
 end
 
-(*s Functor [Make] returns some search functions given a search problem.
+(** {6 Sect } *)
+(** Functor [Make] returns some search functions given a search problem.
     Search functions raise [Not_found] if no success is found.
     States are always visited in the order they appear in the
     output of [branching] (whatever the search method is).
diff --git a/lib/flags.mli b/lib/flags.mli
index 50ba923b74..404cc2d855 100644
--- a/lib/flags.mli
+++ b/lib/flags.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*)
 
-(* Global options of the system. *)
+(** Global options of the system. *)
 
 val boot : bool ref
 
@@ -55,40 +55,40 @@ val if_warn : ('a -> unit) -> 'a -> unit
 
 val hash_cons_proofs : bool ref
 
-(* Temporary activate an option (to activate option [o] on [f x y z],
+(** Temporary activate an option (to activate option [o] on [f x y z],
    use [with_option o (f x y) z]) *)
 val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
-(* Temporary deactivate an option *)
+(** Temporary deactivate an option *)
 val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 
-(* If [None], no limit *)
+(** If [None], no limit *)
 val set_print_hyps_limit : int option -> unit
 val print_hyps_limit : unit -> int option
 
 val add_unsafe : string -> unit
 val is_unsafe : string -> bool
 
-(* Options for the virtual machine *)
+(** Options for the virtual machine *)
 
 val set_boxed_definitions : bool -> unit
 val boxed_definitions : unit -> bool
 
-(* Options for external tools *)
+(** Options for external tools *)
 
-(* Returns string format for default browser to use from Coq or CoqIDE *)
+(** Returns string format for default browser to use from Coq or CoqIDE *)
 val browser_cmd_fmt : string
 
 val is_standard_doc_url : string -> bool
 
-(* Substitute %s in the first chain by the second chain *)
+(** Substitute %s in the first chain by the second chain *)
 val subst_command_placeholder : string -> string -> string
 
-(* Options for specifying where coq librairies reside *)
+(** Options for specifying where coq librairies reside *)
 val coqlib_spec : bool ref
 val coqlib : string ref
 
-(* Options for specifying where OCaml binaries reside *)
+(** Options for specifying where OCaml binaries reside *)
 val camlbin_spec : bool ref
 val camlbin : string ref
 val camlp4bin_spec : bool ref
diff --git a/lib/fmap.mli b/lib/fmap.mli
index c323b0558f..2c8dedd7ee 100644
--- a/lib/fmap.mli
+++ b/lib/fmap.mli
@@ -14,7 +14,7 @@ val iter : (key -> 'a -> unit) -> 'a t -> unit
 val map : ('a -> 'b) -> 'a t -> 'b t
 val fold : (key -> 'a -> 'c -> 'c) -> 'a t -> 'c -> 'c
 
-(* Additions with respect to ocaml standard library. *)
+(** Additions with respect to ocaml standard library. *)
 
 val dom : 'a t -> key list
 val rng : 'a t -> 'a list
diff --git a/lib/gmap.mli b/lib/gmap.mli
index ac1a9922fc..7c86120c68 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.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*)
 
-(* Maps using the generic comparison function of ocaml. Same interface as
+(** Maps using the generic comparison function of ocaml. Same interface as
    the module [Map] from the ocaml standard library. *)
 
 type ('a,'b) t
@@ -23,7 +23,7 @@ val iter : ('a -> 'b -> unit) -> ('a,'b) t -> unit
 val map : ('b -> 'c) -> ('a,'b) t -> ('a,'c) t
 val fold : ('a -> 'b -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c
 
-(* Additions with respect to ocaml standard library. *)
+(** Additions with respect to ocaml standard library. *)
 
 val dom : ('a,'b) t -> 'a list
 val rng : ('a,'b) t -> 'b list
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index 5a5c9a2a4c..349774073a 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.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*)
 
-(* Maps from ['a] to lists of ['b]. *)
+(** Maps from ['a] to lists of ['b]. *)
 
 type ('a,'b) t
 
diff --git a/lib/gset.mli b/lib/gset.mli
index 78fc61e142..0b80176d51 100644
--- a/lib/gset.mli
+++ b/lib/gset.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*)
 
-(* Sets using the generic comparison function of ocaml. Same interface as
+(** Sets using the generic comparison function of ocaml. Same interface as
    the module [Set] from the ocaml standard library. *)
 
 type 'a t
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 243368d004..ca66730b2c 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.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*)
 
-(* Generic hash-consing. *)
+(** Generic hash-consing. *)
 
 module type Comp =
   sig
@@ -37,7 +37,7 @@ val recursive2_hcons :
     (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
       'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
 
-(* Declaring and reinitializing global hash-consing functions *)
+(** Declaring and reinitializing global hash-consing functions *)
 
 val init : unit -> unit
 val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
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
diff --git a/lib/option.mli b/lib/option.mli
index ef2e311a62..3711a2efd7 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -1,12 +1,12 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(* $Id$ *)
+(***********************************************************************
+    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        
+  ***********************************************************************)
+
+(** {% $ %}Id: option.mli 12603 2009-12-21 11:16:27Z herbelin {% $ %} *)
 
 (** Module implementing basic combinators for OCaml option type.
    It tries follow closely the style of OCaml standard library.
diff --git a/lib/pp.mli b/lib/pp.mli
index 66d9bfa674..6ddfa6fc9c 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,30 +1,28 @@
-(************************************************************************)
-(*  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*)
 
-(*i*)
 open Pp_control
-(*i*)
 
-(* Modify pretty printing functions behavior for emacs ouput (special
+(** Modify pretty printing functions behavior for emacs ouput (special
    chars inserted at some places). This function should called once in
    module [Options], that's all. *)
 val make_pp_emacs:unit -> unit
 val make_pp_nonemacs:unit -> unit
 
-(* Pretty-printers. *)
+(** Pretty-printers. *)
 
 type ppcmd
 
 type std_ppcmds = ppcmd Stream.t
 
-(*s Formatting commands. *)
+(** {6 Formatting commands. } *)
 
 val str  : string -> std_ppcmds
 val stras : int * string -> std_ppcmds
@@ -40,11 +38,11 @@ val ismt : std_ppcmds -> bool
 val comment : int -> std_ppcmds
 val comments : ((int * int) * string) list ref
 
-(*s Concatenation. *)
+(** {6 Concatenation. } *)
 
 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
 
-(*s Derived commands. *)
+(** {6 Derived commands. } *)
 
 val spc : unit -> std_ppcmds
 val cut : unit -> std_ppcmds
@@ -59,7 +57,7 @@ val strbrk : string -> std_ppcmds
 
 val xmlescape : ppcmd -> ppcmd
 
-(*s Boxing commands. *)
+(** {6 Boxing commands. } *)
 
 val h : int -> std_ppcmds -> std_ppcmds
 val v : int -> std_ppcmds -> std_ppcmds
@@ -67,7 +65,7 @@ val hv : int -> std_ppcmds -> std_ppcmds
 val hov : int -> std_ppcmds -> std_ppcmds
 val t : std_ppcmds -> std_ppcmds
 
-(*s Opening and closing of boxes. *)
+(** {6 Opening and closing of boxes. } *)
 
 val hb : int -> std_ppcmds
 val vb : int -> std_ppcmds
@@ -77,7 +75,7 @@ val tb : unit -> std_ppcmds
 val close : unit -> std_ppcmds
 val tclose : unit -> std_ppcmds
 
-(*s Pretty-printing functions \emph{without flush}. *)
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%}. } *)
 
 val pp_with : Format.formatter -> std_ppcmds -> unit
 val ppnl_with : Format.formatter -> std_ppcmds -> unit
@@ -87,28 +85,29 @@ val pp_flush_with : Format.formatter -> unit -> unit
 
 val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
 
-(*s Pretty-printing functions \emph{with flush}. *)
+(** {6 Pretty-printing functions {% \emph{%}with flush{% }%}. } *)
 
 val msg_with : Format.formatter -> std_ppcmds -> unit
 val msgnl_with : Format.formatter -> std_ppcmds -> unit
 
 
-(*s The following functions are instances of the previous ones on
+(** {6 Sect } *)
+(** The following functions are instances of the previous ones on
   [std_ft] and [err_ft]. *)
 
-(*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *)
+(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
 
 val pp : std_ppcmds -> unit
 val ppnl : std_ppcmds -> unit
 val pperr : std_ppcmds -> unit
 val pperrnl : std_ppcmds -> unit
-val message : string -> unit       (* = pPNL *)
+val message : string -> unit       (** = pPNL *)
 val warning : string -> unit
 val warn : std_ppcmds -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
-(*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *)
+(** {6 Pretty-printing functions {% \emph{%}with flush{% }%} on [stdout] and [stderr]. } *)
 
 val msg : std_ppcmds -> unit
 val msgnl : std_ppcmds -> unit
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 5c481b89af..83ee7a0f36 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.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*)
 
-(* Parameters of pretty-printing. *)
+(** Parameters of pretty-printing. *)
 
 type pp_global_params = {
   margin : int;
@@ -23,7 +23,7 @@ val set_dflt_gp : Format.formatter -> unit
 val get_gp : Format.formatter -> pp_global_params
 
 
-(*s Output functions of pretty-printing. *)
+(** {6 Output functions of pretty-printing. } *)
 
 type 'a pp_formatter_params = {
   fp_output : out_channel;
@@ -40,7 +40,7 @@ val std_ft : Format.formatter ref
 val err_ft : Format.formatter ref
 val deep_ft : Format.formatter ref
 
-(*s For parametrization through vernacular. *)
+(** {6 For parametrization through vernacular. } *)
 
 val set_depth_boxes : int option -> unit
 val get_depth_boxes : unit -> int option
diff --git a/lib/predicate.mli b/lib/predicate.mli
index 41d5399b97..862479ec40 100644
--- a/lib/predicate.mli
+++ b/lib/predicate.mli
@@ -1,9 +1,9 @@
 
 (*i $Id$ i*)
 
-(* Module [Pred]: sets over infinite ordered types with complement. *)
+(** Module [Pred]: sets over infinite ordered types with complement. *)
 
-(* This module implements the set data structure, given a total ordering
+(** This module implements the set data structure, given a total ordering
    function over the set elements. All operations over sets
    are purely applicative (no side-effects).
    The implementation uses the Set library. *)
@@ -13,7 +13,7 @@ module type OrderedType =
     type t
     val compare: t -> t -> int
   end
-          (* The input signature of the functor [Pred.Make].
+          (** The input signature of the functor [Pred.Make].
              [t] is the type of the set elements.
              [compare] is a total ordering function over the set elements.
              This is a two-argument function [f] such that
@@ -26,44 +26,44 @@ module type OrderedType =
 module type S =
   sig
     type elt
-          (* The type of the set elements. *)
+          (** The type of the set elements. *)
     type t
-          (* The type of sets. *)
+          (** The type of sets. *)
     val empty: t
-          (* The empty set. *)
+          (** The empty set. *)
     val full: t
-          (* The whole type. *)
+          (** The whole type. *)
     val is_empty: t -> bool
-        (* Test whether a set is empty or not. *)
+        (** Test whether a set is empty or not. *)
     val is_full: t -> bool
-        (* Test whether a set contains the whole type or not. *)
+        (** Test whether a set contains the whole type or not. *)
     val mem: elt -> t -> bool
-        (* [mem x s] tests whether [x] belongs to the set [s]. *)
+        (** [mem x s] tests whether [x] belongs to the set [s]. *)
     val singleton: elt -> t
-        (* [singleton x] returns the one-element set containing only [x]. *)
+        (** [singleton x] returns the one-element set containing only [x]. *)
     val add: elt -> t -> t
-        (* [add x s] returns a set containing all elements of [s],
+        (** [add x s] returns a set containing all elements of [s],
            plus [x]. If [x] was already in [s], [s] is returned unchanged. *)
     val remove: elt -> t -> t
-        (* [remove x s] returns a set containing all elements of [s],
+        (** [remove x s] returns a set containing all elements of [s],
            except [x]. If [x] was not in [s], [s] is returned unchanged. *)
     val union: t -> t -> t
     val inter: t -> t -> t
     val diff: t -> t -> t
     val complement: t -> t
-        (* Union, intersection, difference and set complement. *)
+        (** Union, intersection, difference and set complement. *)
     val equal: t -> t -> bool
-        (* [equal s1 s2] tests whether the sets [s1] and [s2] are
+        (** [equal s1 s2] tests whether the sets [s1] and [s2] are
            equal, that is, contain equal elements. *)
     val subset: t -> t -> bool
-        (* [subset s1 s2] tests whether the set [s1] is a subset of
+        (** [subset s1 s2] tests whether the set [s1] is a subset of
            the set [s2]. *)
     val elements: t -> bool * elt list
-        (* Gives a finite representation of the predicate: if the
+        (** Gives a finite representation of the predicate: if the
            boolean is false, then the predicate is given in extension.
            if it is true, then the complement is given *)
   end
 
 module Make(Ord: OrderedType): (S with type elt = Ord.t)
-        (* Functor building an implementation of the set structure
+        (** Functor building an implementation of the set structure
            given a totally ordered type. *)
diff --git a/lib/profile.mli b/lib/profile.mli
index 3647756f71..3d64b79c18 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -1,20 +1,20 @@
-(************************************************************************)
-(*  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*)
 
-(*s This program is a small time and allocation profiler for Objective Caml *)
+(** {6 This program is a small time and allocation profiler for Objective Caml } *)
 
 (*i It requires the UNIX library *)
 
-(* Adapted from Christophe Raffalli *)
+(** Adapted from Christophe Raffalli *)
 
-(* To use it, link it with the program you want to profile (do not forget
+(** To use it, link it with the program you want to profile (do not forget
 "-cclib -lunix -custom unix.cma" among the link options).
 
 To trace a function "f" you first need to get a key for it by using :
@@ -107,23 +107,23 @@ val profile7 :
     -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
 
 
-(* Some utilities to compute the logical and physical sizes and depth
+(** Some utilities to compute the logical and physical sizes and depth
    of ML objects *)
 
-(* Print logical size (in words) and depth of its argument *)
-(* This function does not disturb the heap *)
+(** Print logical size (in words) and depth of its argument 
+   This function does not disturb the heap *)
 val print_logical_stats : 'a -> unit
 
-(* Print physical size, logical size (in words) and depth of its argument *)
-(* This function allocates itself a lot (the same order of magnitude
+(** Print physical size, logical size (in words) and depth of its argument 
+   This function allocates itself a lot (the same order of magnitude
    as the physical size of its argument) *)
 val print_stats : 'a -> unit
 
-(* Return logical size (first for strings, then for not strings),
-   (in words) and depth of its argument *)
-(* This function allocates itself a lot *)
+(** Return logical size (first for strings, then for not strings),
+   (in words) and depth of its argument 
+   This function allocates itself a lot *)
 val obj_stats : 'a -> int * int * int
 
-(* Return physical size of its argument (string part and rest) *)
-(* This function allocates itself a lot *)
+(** Return physical size of its argument (string part and rest) 
+   This function allocates itself a lot *)
 val obj_shared_size : 'a -> int * int
diff --git a/lib/rtree.mli b/lib/rtree.mli
index de5a9aa386..6dd66d104c 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
diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli
index 4aea13e9ad..3258537b99 100644
--- a/lib/segmenttree.mli
+++ b/lib/segmenttree.mli
@@ -7,7 +7,7 @@
 (** A mapping from a union of disjoint segments to some values of type ['a]. *)
 type 'a t
 
-(** [make [(i1, j1), v1; (i2, j2), v2; ...] creates a mapping that
+(** [make [(i1, j1), v1; (i2, j2), v2; ...]] creates a mapping that
     associates to every integer [x] the value [v1] if [i1 <= x <= j1],
     [v2] if [i2 <= x <= j2], and so one. 
     Precondition: the segments must be sorted. *)
diff --git a/lib/system.mli b/lib/system.mli
index cc55f4d66b..8eb3758049 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -1,14 +1,15 @@
-(************************************************************************)
-(*  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*)
 
-(*s Files and load paths. Load path entries remember the original root
+(** {6 Sect } *)
+(** Files and load paths. Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
     [directory]), the root path and the path relative to the root. *)
 
@@ -39,7 +40,8 @@ val exists_dir : string -> bool
 val find_file_in_path :
   ?warn:bool -> load_path -> string -> physical_path * string
 
-(*s Generic input and output functions, parameterized by a magic number
+(** {6 Sect } *)
+(** Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
   when the check fails, with the full file name. *)
 
@@ -54,11 +56,12 @@ val raw_extern_intern : int -> string ->
 val extern_intern : ?warn:bool -> int -> string ->
   (string -> 'a -> unit) * (load_path -> string -> 'a)
 
-(*s Sending/receiving once with external executable *)
+(** {6 Sending/receiving once with external executable } *)
 
 val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
 
-(*s [run_command converter f com] launches command [com], and returns
+(** {6 Sect } *)
+(** [run_command converter f com] launches command [com], and returns
     the contents of stdout and stderr that have been processed with
     [converter]; the processed contents of stdout and stderr is also
     passed to [f] *)
@@ -68,11 +71,11 @@ val run_command : (string -> string) -> (string -> unit) -> string ->
 
 val search_exe_in_path : string -> string option
 
-(*s Time stamps. *)
+(** {6 Time stamps.} *)
 
 type time
 
 val process_time : unit -> float * float
 val get_time : unit -> time
-val time_difference : time -> time -> float (* in seconds *)
+val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.std_ppcmds
diff --git a/lib/tlm.mli b/lib/tlm.mli
index 54eb17599c..05ecee8713 100644
--- a/lib/tlm.mli
+++ b/lib/tlm.mli
@@ -1,28 +1,28 @@
-(************************************************************************)
-(*  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*)
 
-(* Tries. This module implements a data structure [('a,'b) t] mapping lists
+(** Tries. This module implements a data structure [('a,'b) t] mapping lists
    of values of type ['a] to sets (as lists) of values of type ['b]. *)
 
 type ('a,'b) t
 
 val empty : ('a,'b) t
 
-(* Work on labels, not on paths. *)
+(** Work on labels, not on paths. *)
 
 val map : ('a,'b) t -> 'a -> ('a,'b) t
 val xtract : ('a,'b) t -> 'b list
 val dom : ('a,'b) t -> 'a list
 val in_dom : ('a,'b) t -> 'a -> bool
 
-(* Work on paths, not on labels. *)
+(** Work on paths, not on labels. *)
 
 val add : ('a,'b) t -> 'a list * 'b -> ('a,'b) t
 val rmv : ('a,'b) t -> ('a list * 'b) -> ('a,'b) t
diff --git a/lib/tries.mli b/lib/tries.mli
index 342c81ecdc..8e8376772e 100644
--- a/lib/tries.mli
+++ b/lib/tries.mli
@@ -12,7 +12,7 @@ sig
     
   val empty : t
       
-  (* Work on labels, not on paths. *)
+  (** Work on labels, not on paths. *)
 
   val map : t -> Y.t -> t
 
@@ -22,7 +22,7 @@ sig
 
   val in_dom : t -> Y.t -> bool
 
-  (* Work on paths, not on labels. *)
+  (** Work on paths, not on labels. *)
 
   val add : t -> Y.t list * X.t -> t
   
diff --git a/lib/util.mli b/lib/util.mli
index 810e6f0c77..ecf6b0a165 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,21 +1,20 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              
+     \VV/  ************************************************************
+      //   *      This file is distributed under the terms of the      
+           *       GNU Lesser General Public License Version 2.1       
+  **********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Pp
-(*i*)
 
-(* This module contains numerous utility functions on strings, lists,
+(** This module contains numerous utility functions on strings, lists,
    arrays, etc. *)
 
-(*s Errors. [Anomaly] is used for system errors and [UserError] for the
+(** {6 Sect } *)
+(** Errors. [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
 exception Anomaly of string * std_ppcmds
@@ -31,7 +30,7 @@ val alreadydeclared : std_ppcmds -> 'a
 
 exception AnomalyOnError of string * exn
 
-(* [todo] is for running of an incomplete code its implementation is
+(** [todo] is for running of an incomplete code its implementation is
    "do nothing" (or print a message), but this function should not be
    used in a released code *)
 
@@ -53,37 +52,37 @@ val join_loc : loc -> loc -> loc
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
 val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
 
-(* Like [Exc_located], but specifies the outermost file read, the
+(** Like [Exc_located], but specifies the outermost file read, the
    input buffer associated to the location of the error (or the module name
    if boolean is true), and the error itself. *)
 
 exception Error_in_file of string * (bool * string * loc) * exn
 
-(* Mapping under pairs *)
+(** Mapping under pairs *)
 
 val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
 
-(* Mapping under triple *)
+(** Mapping under triple *)
 
 val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
 val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd
 val on_pi3 : ('a -> 'b) -> 'c * 'd * 'a -> 'c * 'd * 'b
 
-(*s Projections from triplets *)
+(** {6 Projections from triplets } *)
 
 val pi1 : 'a * 'b * 'c -> 'a
 val pi2 : 'a * 'b * 'c -> 'b
 val pi3 : 'a * 'b * 'c -> 'c
 
-(*s Chars. *)
+(** {6 Chars. } *)
 
 val is_letter : char -> bool
 val is_digit : char -> bool
 val is_ident_tail : char -> bool
 val is_blank : char -> bool
 
-(*s Strings. *)
+(** {6 Strings. } *)
 
 val explode : string -> string list
 val implode : string list -> string
@@ -109,7 +108,7 @@ val check_ident : string -> unit
 val check_ident_soft : string -> unit
 val lowercase_first_char_utf8 : string -> string
 
-(*s Lists. *)
+(** {6 Lists. } *)
 
 val list_compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
 val list_add_set : 'a -> 'a list -> 'a list
@@ -119,7 +118,8 @@ val list_union : 'a list -> 'a list -> 'a list
 val list_unionq : 'a list -> 'a list -> 'a list
 val list_subtract : 'a list -> 'a list -> 'a list
 val list_subtractq : 'a list -> 'a list -> 'a list
-(* [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
+
+(** [list_tabulate f n] builds [[f 0; ...; f (n-1)]] *)
 val list_tabulate : (int -> 'a) -> int -> 'a list
 val list_make : int -> 'a -> 'a list
 val list_assign : 'a list -> int -> 'a -> 'a list
@@ -127,7 +127,8 @@ val list_distinct : 'a list -> bool
 val list_duplicates : 'a list -> 'a list
 val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
 val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
-(* [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
+
+(** [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [ f ai == ai], then [list_smartmap f l==l] *)
 val list_smartmap : ('a -> 'a) -> 'a list -> 'a list
 val list_map_left : ('a -> 'b) -> 'a list -> 'b list
@@ -140,11 +141,14 @@ val list_map4 :
   ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
 val list_filter_i :
   (int -> 'a -> bool) -> 'a list -> 'a list
-(* [list_index] returns the 1st index of an element in a list (counting from 1) *)
+
+(** [list_index] returns the 1st index of an element in a list (counting from 1) *)
 val list_index : 'a -> 'a list -> int
-(* [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
+
+(** [list_unique_index x l] returns [Not_found] if [x] doesn't occur exactly once *)
 val list_unique_index : 'a -> 'a list -> int
-(* [list_index0] behaves as [list_index] except that it starts counting at 0 *)
+
+(** [list_index0] behaves as [list_index] except that it starts counting at 0 *)
 val list_index0 : 'a -> 'a list -> int
 val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
@@ -163,7 +167,8 @@ val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 val list_try_find : ('a -> 'b) -> 'a list -> 'b
 val list_uniquize : 'a list -> 'a list
-(* merges two sorted lists and preserves the uniqueness property: *)
+
+(** merges two sorted lists and preserves the uniqueness property: *)
 val list_merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
 val list_subset : 'a list -> 'a list -> bool
 val list_chop : int -> 'a list -> 'a list * 'a list
@@ -178,30 +183,38 @@ val list_skipn : int -> 'a list -> 'a list
 val list_skipn_at_least : int -> 'a list -> 'a list
 val list_addn : int -> 'a -> 'a list -> 'a list
 val list_prefix_of : 'a list -> 'a list -> bool
-(* [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
+
+(** [list_drop_prefix p l] returns [t] if [l=p++t] else return [l] *)
 val list_drop_prefix : 'a list -> 'a list -> 'a list
 val list_drop_last : 'a list -> 'a list
-(* [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
+
+(** [map_append f [x1; ...; xn]] returns [(f x1)@(f x2)@...@(f xn)] *)
 val list_map_append : ('a -> 'b list) -> 'a list -> 'b list
 val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
-(* raises [Invalid_argument] if the two lists don't have the same length *)
+
+(** raises [Invalid_argument] if the two lists don't have the same length *)
 val list_map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
-(* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
+
+(** [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
    where [(e_i,k_i)=f e_{i-1} l_i] *)
 val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
 val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
 val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
-(* A generic cartesian product: for any operator (**),
+
+(** A generic cartesian product: for any operator (**),
    [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]],
    and so on if there are more elements in the lists. *)
 val list_cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-(* [list_cartesians] is an n-ary cartesian product: it iterates
+
+(** [list_cartesians] is an n-ary cartesian product: it iterates
    [list_cartesian] over a list of lists.  *)
 val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
-(* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
+
+(** list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
-(* Keep only those products that do not return None *)
+
+(** Keep only those products that do not return None *)
 val list_cartesian_filter :
   ('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
 val list_cartesians_filter :
@@ -209,7 +222,7 @@ val list_cartesians_filter :
 
 val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 
-(*s Arrays. *)
+(** {6 Arrays. } *)
 
 val array_compare : ('a -> 'a -> int) -> 'a array -> 'a array -> int
 val array_exists : ('a -> bool) -> 'a array -> bool
@@ -258,11 +271,11 @@ val array_distinct : 'a array -> bool
 val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 val array_rev_to_list : 'a array -> 'a list
 
-(*s Matrices *)
+(** {6 Matrices } *)
 
 val matrix_transpose : 'a list list -> 'a list list
 
-(*s Functions. *)
+(** {6 Functions. } *)
 
 val identity : 'a -> 'a
 val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
@@ -271,7 +284,7 @@ val iterate : ('a -> 'a) -> int -> 'a -> 'a
 val repeat : int -> ('a -> unit) -> 'a -> unit
 val iterate_for : int -> int -> (int -> 'a -> 'a) -> 'a -> 'a
 
-(*s Misc. *)
+(** {6 Misc. } *)
 
 type ('a,'b) union = Inl of 'a | Inr of 'b
 
@@ -286,12 +299,12 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list
 val interval : int -> int -> int list
 
 
-(* In [map_succeed f l] an element [a] is removed if [f a] raises *)
-(* [Failure _] otherwise behaves as [List.map f l] *)
+(** In [map_succeed f l] an element [a] is removed if [f a] raises 
+   [Failure _] otherwise behaves as [List.map f l] *)
 
 val map_succeed : ('a -> 'b) -> 'a list -> 'b list
 
-(*s Pretty-printing. *)
+(** {6 Pretty-printing. } *)
 
 val pr_spc : unit -> std_ppcmds
 val pr_fnl : unit -> std_ppcmds
@@ -306,7 +319,8 @@ val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val nth : int -> std_ppcmds
 
 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-(* unlike all other functions below, [prlist] works lazily.
+
+(** unlike all other functions below, [prlist] works lazily.
    if a strict behavior is needed, use [prlist_strict] instead. *)
 val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prlist_with_sep :
@@ -321,34 +335,36 @@ val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
 val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val surround : std_ppcmds -> std_ppcmds
 
-(*s Memoization. *)
+(** {6 Memoization. } *)
 
-(* General comments on memoization:
+(** General comments on memoization:
    - cache is created whenever the function is supplied (because of
       ML's polymorphic value restriction).
    - cache is never flushed (unless the memoized fun is GC'd)
- *)
-(* One cell memory: memorizes only the last call *)
+ 
+   One cell memory: memorizes only the last call *)
 val memo1_1 : ('a -> 'b) -> ('a -> 'b)
 val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
-(* with custom equality (used to deal with various arities) *)
+
+(** with custom equality (used to deal with various arities) *)
 val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b)
 
-(* Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
+(** Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
 val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b)
 
-(*s Size of an ocaml value (in words, bytes and kilobytes). *)
+(** {6 Size of an ocaml value (in words, bytes and kilobytes). } *)
 
 val size_w : 'a -> int
 val size_b : 'a -> int
 val size_kb : 'a -> int
 
-(*s Total size of the allocated ocaml heap. *)
+(** {6 Total size of the allocated ocaml heap. } *)
 
 val heap_size : unit -> int
 val heap_size_kb : unit -> int
 
-(*s Coq interruption: set the following boolean reference to interrupt Coq
+(** {6 Sect } *)
+(** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)
 
 val interrupt : bool ref