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

24 files changed, 321 insertions, 343 deletions

diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 855f023f57..901ddb7218 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(*  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        
+  ***********************************************************************)
 
 open Term
 open Names
@@ -14,7 +14,12 @@ open Sign
 open Proof_type
 open Ind_tables
 
-(* Build boolean equality of a block of mutual inductive types *)
+(** This file is about the automatic generation of schemes about
+    decidable equality,
+    @author Vincent Siles
+    Oct 2007 *)
+
+(** {6 Build boolean equality of a block of mutual inductive types } *)
 
 exception EqNotFound of inductive * inductive
 exception EqUnknown of string
@@ -27,7 +32,7 @@ exception NonSingletonProp of inductive
 val beq_scheme_kind : mutual scheme_kind
 val build_beq_scheme : mutual_inductive -> constr array
 
-(* Build equivalence between boolean equality and Leibniz equality *)
+(** {6 Build equivalence between boolean equality and Leibniz equality } *)
 
 val lb_scheme_kind : mutual scheme_kind
 val make_lb_scheme : mutual_inductive -> constr array
@@ -35,7 +40,7 @@ val make_lb_scheme : mutual_inductive -> constr array
 val bl_scheme_kind : mutual scheme_kind
 val make_bl_scheme : mutual_inductive -> constr array
 
-(* Build decidability of equality *)
+(** {6 Build decidability of equality } *)
 
 val eq_dec_scheme_kind : mutual scheme_kind
 val make_eq_decidability : mutual_inductive -> constr array
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
index 3866fff39f..b6cde8cf64 100644
--- a/toplevel/autoinstance.mli
+++ b/toplevel/autoinstance.mli
@@ -1,38 +1,36 @@
-(************************************************************************)
-(*  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:{% $ %} *)
 
-(*i*)
 open Term
 open Libnames
 open Typeclasses
 open Names
 open Evd
 open Sign
-(*i*)
 
-(*s Automatic detection of (some) record instances *)
+(** {6 Automatic detection of (some) record instances } *)
 
-(* What to do if we find an instance. Passed are : the reference
+(** What to do if we find an instance. Passed are : the reference
  * representing the record/class (definition or constructor) *)
 type instance_decl_function = global_reference -> rel_context -> constr list -> unit
 
-(* [search_declaration gr] Search in the library if the (new)
+(** [search_declaration gr] Search in the library if the (new)
  * declaration gr can form an instance of a registered record/class *)
 val search_declaration : global_reference -> unit
 
-(* [search_record declf gr evm] Search the library for instances of
+(** [search_record declf gr evm] Search the library for instances of
    the (new) record/class declaration [gr], and register them using
    [declf]. [evm] is the signature of the record (to avoid recomputing
    it) *)
 val search_record : instance_decl_function -> global_reference -> evar_map -> unit
 
-(* Instance declaration for both scenarios *)
+(** Instance declaration for both scenarios *)
 val declare_record_instance : instance_decl_function
 val declare_class_instance : instance_decl_function
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 24f37335be..8f26f44951 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -1,19 +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*)
 
-(*i*)
 open Pp
 open Util
-(*i*)
 
-(* Error report. *)
+(** Error report. *)
 
 val print_loc : loc -> std_ppcmds
 
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 3398e3fab5..4ee894cc97 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -1,14 +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        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Names
 open Term
 open Classops
@@ -16,31 +15,30 @@ open Declare
 open Libnames
 open Decl_kinds
 open Nametab
-(*i*)
 
-(* Classes and coercions. *)
+(** Classes and coercions. *)
 
-(* [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
+(** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
    from [src] to [tg] *)
 val try_add_new_coercion_with_target : global_reference -> locality ->
   source:cl_typ -> target:cl_typ ->  unit
 
-(* [try_add_new_coercion ref s] declares [ref], assumed to be of type
+(** [try_add_new_coercion ref s] declares [ref], assumed to be of type
    [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
 val try_add_new_coercion : global_reference -> locality -> unit
 
-(* [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
+(** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
    transparent constant which unfolds to some class [tg]; it declares
    an identity coercion from [cst] to [tg], named something like
    ["Id_cst_tg"] *)
 val try_add_new_coercion_subclass : cl_typ -> locality -> unit
 
-(* [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
+(** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
    from [src] to [tg] where the target is inferred from the type of [ref] *)
 val try_add_new_coercion_with_source : global_reference -> locality ->
   source:cl_typ -> unit
 
-(* [try_add_new_identity_coercion id s src tg] enriches the
+(** [try_add_new_identity_coercion id s src tg] enriches the
    environment with a new definition of name [id] declared as an
    identity coercion from [src] to [tg] *)
 val try_add_new_identity_coercion : identifier -> locality ->
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index b8b104d47a..279622843f 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -1,14 +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        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Names
 open Decl_kinds
 open Term
@@ -22,36 +21,35 @@ open Util
 open Typeclasses
 open Implicit_quantifiers
 open Libnames
-(*i*)
 
-(* Errors *)
+(** Errors *)
 
 val mismatched_params : env -> constr_expr list -> rel_context -> 'a
 
 val mismatched_props : env -> constr_expr list -> rel_context -> 'a
 
-(* Post-hoc class declaration. *)
+(** Post-hoc class declaration. *)
 
 val declare_class : reference -> unit
 
-(* Instance declaration *)
+(** Instance declaration *)
 
 val declare_instance : bool -> reference -> unit
 
 val declare_instance_constant :
   typeclass ->
-  int option -> (* priority *)
-  bool -> (* globality *)
-  Impargs.manual_explicitation list -> (* implicits *)
+  int option -> (** priority *)
+  bool -> (** globality *)
+  Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Libnames.global_reference -> unit) ->
-  identifier -> (* name *)
-  Term.constr -> (* body *)
-  Term.types -> (* type *)
+  identifier -> (** name *)
+  Term.constr -> (** body *)
+  Term.types -> (** type *)
   Names.identifier
 
 val new_instance :
-  ?abstract:bool -> (* Not abstract by default. *)
-  ?global:bool -> (* Not global by default. *)
+  ?abstract:bool -> (** Not abstract by default. *)
+  ?global:bool -> (** Not global by default. *)
   local_binder list ->
   typeclass_constraint ->
   constr_expr ->
@@ -61,20 +59,20 @@ val new_instance :
   int option ->
   identifier
 
-(* Setting opacity *)
+(** Setting opacity *)
 
 val set_typeclass_transparency : evaluable_global_reference -> bool -> unit
 
-(* For generation on names based on classes only *)
+(** For generation on names based on classes only *)
 
 val id_of_class : typeclass -> identifier
 
-(* Context command *)
+(** Context command *)
 
 val context : ?hook:(Libnames.global_reference -> unit) ->
   local_binder list -> unit
 
-(* Forward ref for refine *)
+(** Forward ref for refine *)
 
 val refine_ref : (open_constr -> Proof_type.tactic) ref
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 48fc5a8ebc..904a1a034e 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -1,14 +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        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Util
 open Names
 open Term
@@ -21,19 +20,19 @@ open Decl_kinds
 open Redexpr
 open Constrintern
 open Pfedit
-(*i*)
 
-(*s This file is about the interpretation of raw commands into typed
+(** {6 Sect } *)
+(** This file is about the interpretation of raw commands into typed
     ones and top-level declaration of the main Gallina objects *)
 
-(* Hooks for Pcoq *)
+(** Hooks for Pcoq *)
 
 val set_declare_definition_hook : (definition_entry -> unit) -> unit
 val get_declare_definition_hook : unit -> (definition_entry -> unit)
 val set_declare_assumptions_hook : (types -> unit) -> unit
 
-(*************************************************************************)
-(* Definitions/Let *)
+(************************************************************************
+   Definitions/Let *)
 
 val interp_definition :
   boxed_flag -> local_binder list -> red_expr option -> constr_expr ->
@@ -42,24 +41,24 @@ val interp_definition :
 val declare_definition : identifier -> locality * definition_object_kind ->
   definition_entry -> manual_implicits -> declaration_hook -> unit
 
-(*************************************************************************)
-(* Parameters/Assumptions *)
+(************************************************************************
+   Parameters/Assumptions *)
 
 val interp_assumption :
   local_binder list -> constr_expr -> types * manual_implicits
 
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   manual_implicits ->
-  bool (* implicit *) -> bool (* inline *) -> variable located -> unit
+  bool (** implicit *) -> bool (* inline *) -> variable located -> unit
 
 val declare_assumptions : variable located list ->
   coercion_flag -> assumption_kind -> types -> manual_implicits ->
   bool -> bool -> unit
 
-(*************************************************************************)
-(* Inductive and coinductive types *)
+(************************************************************************
+   Inductive and coinductive types *)
 
-(* Extracting the semantical components out of the raw syntax of mutual
+(** Extracting the semantical components out of the raw syntax of mutual
    inductive declarations *)
 
 type structured_one_inductive_expr = {
@@ -75,30 +74,30 @@ val extract_mutual_inductive_declaration_components :
   (one_inductive_expr * decl_notation list) list ->
     structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
 
-(* Typing mutual inductive definitions *)
+(** Typing mutual inductive definitions *)
 
 type one_inductive_impls =
-  Impargs.manual_explicitation list (* for inds *)*
-  Impargs.manual_explicitation list list (* for constrs *)
+  Impargs.manual_explicitation list (** for inds *)*
+  Impargs.manual_explicitation list list (** for constrs *)
 
 val interp_mutual_inductive :
   structured_inductive_expr -> decl_notation list -> bool ->
     mutual_inductive_entry * one_inductive_impls list
 
-(* Registering a mutual inductive definition together with its
+(** Registering a mutual inductive definition together with its
    associated schemes *)
 
 val declare_mutual_inductive_with_eliminations :
   bool -> mutual_inductive_entry -> one_inductive_impls list ->
   mutual_inductive
 
-(* Entry points for the vernacular commands Inductive and CoInductive *)
+(** Entry points for the vernacular commands Inductive and CoInductive *)
 
 val do_mutual_inductive :
   (one_inductive_expr * decl_notation list) list -> bool -> unit
 
-(*************************************************************************)
-(* Fixpoints and cofixpoints *)
+(************************************************************************
+   Fixpoints and cofixpoints *)
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
@@ -107,19 +106,19 @@ type structured_fixpoint_expr = {
   fix_type : constr_expr
 }
 
-(* Extracting the semantical components out of the raw syntax of
+(** Extracting the semantical components out of the raw syntax of
    (co)fixpoints declarations *)
 
 val extract_fixpoint_components :
   (fixpoint_expr * decl_notation list) list ->
     structured_fixpoint_expr list * decl_notation list *
-    (* possible structural arg: *) lident option list
+    (** possible structural arg: *) lident option list
 
 val extract_cofixpoint_components :
   (cofixpoint_expr * decl_notation list) list ->
     structured_fixpoint_expr list * decl_notation list
 
-(* Typing global fixpoints and cofixpoint_expr *)
+(** Typing global fixpoints and cofixpoint_expr *)
 
 type recursive_preentry =
   identifier list * constr option list * types list
@@ -132,7 +131,7 @@ val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
     recursive_preentry * (int * manual_implicits) list
 
-(* Registering fixpoints and cofixpoints in the environment *)
+(** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   bool -> recursive_preentry * (int * manual_implicits) list -> 
@@ -142,7 +141,7 @@ val declare_cofixpoint :
   bool -> recursive_preentry * (int * manual_implicits) list ->
     decl_notation list -> unit
 
-(* Entry points for the vernacular commands Fixpoint and CoFixpoint *)
+(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
   (fixpoint_expr * decl_notation list) list -> bool -> unit
@@ -150,7 +149,7 @@ val do_fixpoint :
 val do_cofixpoint :
   (cofixpoint_expr * decl_notation list) list -> bool -> unit
 
-(* Utils *)
+(** Utils *)
 
 val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit
 
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index f4c82a41e0..9258594586 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.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*)
 
-(* Initialization. *)
+(** Initialization. *)
 
 val set_debug : unit -> unit
 
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 87f4bdeb55..0c43cc757c 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -1,21 +1,21 @@
-(************************************************************************)
-(*  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*)
 
-(* The Coq main module. The following function [start] will parse the
+(** The Coq main module. The following function [start] will parse the
    command line, print the banner, initialize the load path, load the input
    state, load the files given on the command line, load the ressource file,
    produce the output state if any, and finally will launch [Toplevel.loop]. *)
 
 val start : unit -> unit
 
-(* [init_ide] is to be used by the Coq IDE.
+(** [init_ide] is to be used by the Coq IDE.
    It does everything [start] does, except launching the toplevel loop.
    It returns the list of Coq files given on the command line. *)
 
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index c6496cd4b0..b3636d7176 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(*  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*)
 
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 848fec79c2..23c10767dc 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -1,14 +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        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Pp
 open Names
 open Indtypes
@@ -19,9 +18,8 @@ open Typeclasses_errors
 open Indrec
 open Cases
 open Logic
-(*i*)
 
-(* This module provides functions to explain the type errors. *)
+(** This module provides functions to explain the type errors. *)
 
 val explain_type_error : env -> type_error -> std_ppcmds
 
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 57ebbcda17..2abd15ce3b 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(*  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        
+  ***********************************************************************)
 
 open Term
 open Names
@@ -13,10 +13,10 @@ open Mod_subst
 open Sign
 open Declarations
 
-(* This module provides support for registering inductive scheme builders,
+(** This module provides support for registering inductive scheme builders,
    declaring schemes and generating schemes on demand *)
 
-(* A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *)
+(** A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *)
 
 type mutual
 type individual
@@ -25,7 +25,7 @@ type 'a scheme_kind
 type mutual_scheme_object_function = mutual_inductive -> constr array
 type individual_scheme_object_function = inductive -> constr
 
-(* Main functions to register a scheme builder *)
+(** Main functions to register a scheme builder *)
 
 val declare_mutual_scheme_object : string -> ?aux:string ->
   mutual_scheme_object_function -> mutual scheme_kind
@@ -37,15 +37,15 @@ val declare_individual_scheme_object : string -> ?aux:string ->
 val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
 *)
 
-(* Force generation of a (mutually) scheme with possibly user-level names *)
+(** Force generation of a (mutually) scheme with possibly user-level names *)
 
-val define_individual_scheme : individual scheme_kind -> bool (* internal *) ->
+val define_individual_scheme : individual scheme_kind -> bool (** internal *) ->
   identifier option -> inductive -> constant
 
-val define_mutual_scheme : mutual scheme_kind -> bool (* internal *) ->
+val define_mutual_scheme : mutual scheme_kind -> bool (** internal *) ->
   (int * identifier) list -> mutual_inductive -> constant array
 
-(* Main function to retrieve a scheme in the cache or to generate it *)
+(** Main function to retrieve a scheme in the cache or to generate it *)
 val find_scheme : 'a scheme_kind -> inductive -> constant
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 9aa32b7bd6..aab60a590d 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -1,14 +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        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Util
 open Names
 open Term
@@ -18,39 +17,38 @@ open Rawterm
 open Genarg
 open Vernacexpr
 open Ind_tables
-(*i*)
 
-(* See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
+(** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
 
-(* Build and register the boolean equalities associated to an inductive type *)
+(** Build and register the boolean equalities associated to an inductive type *)
 
 val declare_beq_scheme : mutual_inductive -> unit
 
 val declare_eq_decidability : mutual_inductive -> unit
 
-(* Build and register a congruence scheme for an equality-like inductive type *)
+(** Build and register a congruence scheme for an equality-like inductive type *)
 
 val declare_congr_scheme : inductive -> unit
 
-(* Build and register rewriting schemes for an equality-like inductive type *)
+(** Build and register rewriting schemes for an equality-like inductive type *)
 
 val declare_rewriting_schemes : inductive -> unit
 
-(* Mutual Minimality/Induction scheme *)
+(** Mutual Minimality/Induction scheme *)
 
 val do_mutual_induction_scheme :
   (identifier located * bool * inductive * rawsort) list -> unit
 
-(* Main calls to interpret the Scheme command *)
+(** Main calls to interpret the Scheme command *)
 
 val do_scheme : (identifier located option * scheme) list -> unit
 
-(* Combine a list of schemes into a conjunction of them *)
+(** Combine a list of schemes into a conjunction of them *)
 
 val build_combined_scheme : env -> constant list -> constr * types
 
 val do_combined_scheme : identifier located -> identifier located list -> unit
 
-(* Hook called at each inductive type definition *)
+(** Hook called at each inductive type definition *)
 
 val declare_default_schemes : mutual_inductive -> unit
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index f4e9f6f587..44502b4e42 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -1,14 +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.fix_expr        *)
-(************************************************************************)
+(***********************************************************************
+    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.fix_expr        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Names
 open Term
 open Decl_kinds
@@ -17,9 +16,8 @@ open Tacexpr
 open Vernacexpr
 open Proof_type
 open Pfedit
-(*i*)
 
-(* A hook start_proof calls on the type of the definition being started *)
+(** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
 val start_proof : identifier -> goal_kind -> types ->
@@ -35,31 +33,32 @@ val start_proof_with_initialization :
   (identifier * (types * (int * Impargs.manual_explicitation list))) list ->
   declaration_hook -> unit
 
-(* A hook the next three functions pass to cook_proof *)
+(** A hook the next three functions pass to cook_proof *)
 val set_save_hook : (Proof.proof -> unit) -> unit
 
-(*s [save_named b] saves the current completed proof under the name it
+(** {6 Sect } *)
+(** [save_named b] saves the current completed proof under the name it
 was started; boolean [b] tells if the theorem is declared opaque; it
 fails if the proof is not completed *)
 
 val save_named : bool -> unit
 
-(* [save_anonymous b name] behaves as [save_named] but declares the theorem
+(** [save_anonymous b name] behaves as [save_named] but declares the theorem
 under the name [name] and respects the strength of the declaration *)
 
 val save_anonymous : bool -> identifier -> unit
 
-(* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
+(** [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
    declares the theorem under the name [name] and gives it the
    strength [strength] *)
 
 val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit
 
-(* [admit ()] aborts the current goal and save it as an assmumption *)
+(** [admit ()] aborts the current goal and save it as an assmumption *)
 
 val admit : unit -> unit
 
-(* [get_current_context ()] returns the evar context and env of the
+(** [get_current_context ()] returns the evar context and env of the
    current open proof if any, otherwise returns the empty evar context
    and the current global env *)
 
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli
index d57ecb9483..07d826933c 100644
--- a/toplevel/libtypes.mli
+++ b/toplevel/libtypes.mli
@@ -1,31 +1,27 @@
-(************************************************************************)
-(*  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:{% $ %} *)
 
-(*i*)
 open Term
-(*i*)
 
-(*
- * Persistent library of all declared object,
- * indexed by their types (uses Dnets)
- *)
+(** Persistent library of all declared object, indexed by their types 
+    (uses Dnets) *)
 
-(* results are the reference of the object, together with a context
+(** results are the reference of the object, together with a context
 (constr+evar) and a substitution under this context *)
 type result = Libnames.global_reference * (constr*existential_key) * Termops.subst
 
-(* this is the reduction function used in the indexing process *)
+(** this is the reduction function used in the indexing process *)
 val reduce : types -> types
 
-(* The different types of search available.
- * See term_dnet.mli for more explanations *)
+(** The different types of search available. 
+    See term_dnet.mli for more explanations *)
 val search_pattern : types -> result list
 val search_concl : types -> result list
 val search_head_concl : types -> result list
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index a06806935b..63272b7d3e 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -1,14 +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        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Util
 open Names
 open Libnames
@@ -18,16 +17,15 @@ open Tacexpr
 open Vernacexpr
 open Notation
 open Topconstr
-(*i*)
 
 val add_token_obj : string -> unit
 
-(* Adding a tactic notation in the environment *)
+(** Adding a tactic notation in the environment *)
 
 val add_tactic_notation :
   int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit
 
-(* Adding a (constr) notation in the environment*)
+(** Adding a (constr) notation in the environment*)
 
 val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
   constr_expr -> scope_name option -> unit
@@ -35,32 +33,32 @@ val add_infix : locality_flag -> (lstring * syntax_modifier list) ->
 val add_notation : locality_flag -> constr_expr ->
   (lstring * syntax_modifier list) -> scope_name option -> unit
 
-(* Declaring delimiter keys and default scopes *)
+(** Declaring delimiter keys and default scopes *)
 
 val add_delimiters : scope_name -> string -> unit
 val add_class_scope : scope_name -> Classops.cl_typ -> unit
 
-(* Add only the interpretation of a notation that already has pa/pp rules *)
+(** Add only the interpretation of a notation that already has pa/pp rules *)
 
 val add_notation_interpretation :
   (lstring * constr_expr * scope_name option) -> unit
 
-(* Add a notation interpretation for supporting the "where" clause *)
+(** Add a notation interpretation for supporting the "where" clause *)
 
 val set_notation_for_interpretation : Constrintern.full_internalization_env ->
   (lstring * constr_expr * scope_name option) -> unit
 
-(* Add only the parsing/printing rule of a notation *)
+(** Add only the parsing/printing rule of a notation *)
 
 val add_syntax_extension :
   locality_flag -> (lstring * syntax_modifier list) -> unit
 
-(* Add a syntactic definition (as in "Notation f := ...") *)
+(** Add a syntactic definition (as in "Notation f := ...") *)
 
 val add_syntactic_definition : identifier -> identifier list * constr_expr ->
   bool -> bool -> unit
 
-(* Print the Camlp4 state of a grammar *)
+(** Print the Camlp4 state of a grammar *)
 
 val print_grammar : string -> unit
 
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 4230f0ee4b..a03ad6242e 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.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*)
 
-(* If there is a toplevel under Coq, it is described by the following
+(** If there is a toplevel under Coq, it is described by the following
    record. *)
 type toplevel = {
   load_obj : string -> unit;
@@ -16,44 +16,44 @@ type toplevel = {
   add_dir  : string -> unit;
   ml_loop  : unit -> unit }
 
-(* Sets and initializes a toplevel (if any) *)
+(** Sets and initializes a toplevel (if any) *)
 val set_top : toplevel -> unit
 
-(* Are we in a native version of Coq? *)
+(** Are we in a native version of Coq? *)
 val is_native : bool
 
-(* Removes the toplevel (if any) *)
+(** Removes the toplevel (if any) *)
 val remove : unit -> unit
 
-(* Tests if an Ocaml toplevel runs under Coq *)
+(** Tests if an Ocaml toplevel runs under Coq *)
 val is_ocaml_top : unit -> bool
 
-(* Tests if we can load ML files *)
+(** Tests if we can load ML files *)
 val has_dynlink : bool
 
-(* Starts the Ocaml toplevel loop *)
+(** Starts the Ocaml toplevel loop *)
 val ocaml_toploop : unit -> unit
 
-(* Dynamic loading of .cmo *)
+(** Dynamic loading of .cmo *)
 val dir_ml_load : string -> unit
 
-(* Dynamic interpretation of .ml *)
+(** Dynamic interpretation of .ml *)
 val dir_ml_use : string -> unit
 
-(* Adds a path to the ML paths *)
+(** Adds a path to the ML paths *)
 val add_ml_dir : string -> unit
 val add_rec_ml_dir : string -> unit
 
-(* Adds a path to the Coq and ML paths *)
+(** Adds a path to the Coq and ML paths *)
 val add_path : unix_path:string -> coq_root:Names.dir_path -> unit
 val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit
 
-(* List of modules linked to the toplevel *)
+(** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
 val module_is_known : string -> bool
 val load_object : string -> string -> unit
 
-(* Summary of Declared ML Modules *)
+(** Summary of Declared ML Modules *)
 val get_loaded_modules : unit -> string list
 val add_loaded_module : string -> unit
 val init_ml_modules : unit -> unit
diff --git a/toplevel/record.mli b/toplevel/record.mli
index b9864f0837..d432bff6de 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -1,14 +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        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Names
 open Term
 open Sign
@@ -16,9 +15,8 @@ open Vernacexpr
 open Topconstr
 open Impargs
 open Libnames
-(*i*)
 
-(* [declare_projections ref name coers params fields] declare projections of
+(** [declare_projections ref name coers params fields] declare projections of
    record [ref] (if allowed) using the given [name] as argument, and put them
    as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
@@ -28,16 +26,16 @@ val declare_projections :
   (name * bool) list * constant option list
 
 val declare_structure : Decl_kinds.recursivity_kind ->
-  bool (*infer?*) -> identifier -> identifier ->
-  manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *)
-  Impargs.manual_explicitation list list -> rel_context -> (* fields *)
+  bool (**infer?*) -> identifier -> identifier ->
+  manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
+  Impargs.manual_explicitation list list -> rel_context -> (** fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
-  bool -> (* coercion? *)
-  bool list -> (* field coercions *)
+  bool -> (** coercion? *)
+  bool list -> (** field coercions *)
   Evd.evar_map ->
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.recursivity_kind * bool(*infer?*)* lident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
   (local_decl_expr with_coercion with_notation) list *
   identifier * constr_expr option -> global_reference
diff --git a/toplevel/search.mli b/toplevel/search.mli
index cc764fbde1..a9d62c6efa 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(*  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*)
 
@@ -16,7 +16,7 @@ open Pattern
 open Libnames
 open Nametab
 
-(*s Search facilities. *)
+(** {6 Search facilities. } *)
 
 type glob_search_about_item =
   | GlobSearchSubPattern of constr_pattern
@@ -28,14 +28,14 @@ val search_pattern : constr -> dir_path list * bool -> unit
 val search_about  :
   (bool * glob_search_about_item) list -> dir_path list * bool -> unit
 
-(* The filtering function that is by standard search facilities.
+(** The filtering function that is by standard search facilities.
    It can be passed as argument to the raw search functions.
    It is used in pcoq. *)
 
 val filter_by_module_from_list :
   dir_path list * bool -> global_reference -> env -> 'a -> bool
 
-(* raw search functions can be used for various extensions.
+(** raw search functions can be used for various extensions.
    They are also used for pcoq. *)
 val gen_filtered_search : (global_reference -> env -> constr -> bool) ->
       (global_reference -> env -> constr -> unit) -> unit
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 3f2fa83adb..f51c088f04 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -1,46 +1,44 @@
-(************************************************************************)
-(*  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
 open Pcoq
-(*i*)
 
-(* The Coq toplevel loop. *)
+(** The Coq toplevel loop. *)
 
-(* A buffer for the character read from a channel. We store the command
+(** A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
 
 type input_buffer = {
   mutable prompt : unit -> string;
-  mutable str : string; (* buffer of already read characters *)
-  mutable len : int;    (* number of chars in the buffer *)
-  mutable bols : int list; (* offsets in str of begining of lines *)
-  mutable tokens : Pcoq.Gram.parsable; (* stream of tokens *)
-  mutable start : int } (* stream count of the first char of the buffer *)
+  mutable str : string; (** buffer of already read characters *)
+  mutable len : int;    (** number of chars in the buffer *)
+  mutable bols : int list; (** offsets in str of begining of lines *)
+  mutable tokens : Pcoq.Gram.parsable; (** stream of tokens *)
+  mutable start : int } (** stream count of the first char of the buffer *)
 
-(* The input buffer of stdin. *)
+(** The input buffer of stdin. *)
 
 val top_buffer : input_buffer
 val set_prompt : (unit -> string) -> unit
 
-(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
+(** Toplevel error explanation, dealing with locations, Drop, Ctrl-D
   May raise only the following exceptions: [Drop] and [End_of_input],
   meaning we get out of the Coq loop. *)
 
 val print_toplevel_error : exn -> std_ppcmds
 
-(* Parse and execute a vernac command. *)
+(** Parse and execute a vernac command. *)
 
 val do_vernac : unit -> unit
 
-(* Main entry point of Coq: read and execute vernac commands. *)
+(** Main entry point of Coq: read and execute vernac commands. *)
 
 val loop : unit -> unit
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index fb973e3baf..1dfd4897b2 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -1,23 +1,23 @@
-(************************************************************************)
-(*  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 Prints the version number on the standard output and exits (with 0). *)
+(** {6 Prints the version number on the standard output and exits (with 0). } *)
 
 val version : unit -> 'a
 
-(*s Prints the usage on the error output, preceeded by a user-provided message. *)
+(** {6 Prints the usage on the error output, preceeded by a user-provided message. } *)
 val print_usage : string -> unit
 
-(*s Prints the usage on the error output. *)
+(** {6 Prints the usage on the error output. } *)
 val print_usage_coqtop : unit -> unit
 val print_usage_coqc : unit -> unit
 
-(*s Prints the configuration information *)
+(** {6 Prints the configuration information } *)
 val print_config : unit -> unit
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 747c02afe3..8ae319791b 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -1,22 +1,22 @@
-(************************************************************************)
-(*  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*)
 
-(* Parsing of vernacular. *)
+(** Parsing of vernacular. *)
 
-(* Read a vernac command on the specified input (parse only).
+(** Read a vernac command on the specified input (parse only).
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
 val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
  Util.loc * Vernacexpr.vernac_expr
 
-(* Reads and executes vernac commands from a stream.
+(** Reads and executes vernac commands from a stream.
    The boolean [just_parsing] disables interpretation of commands. *)
 
 exception DuringCommandInterp of Util.loc * exn
@@ -27,16 +27,16 @@ val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
 val eval_ctrl : Vernacexpr.vernac_expr -> unit
 val raw_do_vernac : Pcoq.Gram.parsable -> unit
 
-(* Set XML hooks *)
+(** Set XML hooks *)
 val set_xml_start_library : (unit -> unit) -> unit
 val set_xml_end_library   : (unit -> unit) -> unit
 
-(* Load a vernac file, verbosely or not. Errors are annotated with file
+(** Load a vernac file, verbosely or not. Errors are annotated with file
    and location *)
 
 val load_vernac : bool -> string -> unit
 
 
-(* Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
+(** Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
 
 val compile : bool -> string -> unit
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 58df8a9065..fa9f2b7c2a 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -1,34 +1,33 @@
-(************************************************************************)
-(*  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 Names
 open Term
 open Vernacinterp
 open Vernacexpr
 open Topconstr
-(*i*)
 
-(* Vernacular entries *)
+(** Vernacular entries *)
 
 val show_script : unit -> unit
 val show_prooftree : unit -> unit
 
 val show_node : unit -> unit
 
-(* This function can be used by any command that want to observe terms
+(** This function can be used by any command that want to observe terms
    in the context of the current goal, as for instance in pcoq *)
 val get_current_context_of_args : int option -> Evd.evar_map * Environ.env
 
 (*i
-(* this function is used to analyse the extra arguments in search commands.
+
+(** this function is used to analyse the extra arguments in search commands.
    It is used in pcoq. *) (*i anciennement: inside_outside i*)
 val interp_search_restriction : search_restriction -> dir_path list * bool
 i*)
@@ -47,7 +46,7 @@ type pcoq_hook = {
 
 val set_pcoq_hook : pcoq_hook -> unit
 
-(* This function makes sure that the function given in argument is preceded
+(** This function makes sure that the function given in argument is preceded
    by a command aborting all proofs if necessary.
    It is used in pcoq. *)
 val abort_refine : ('a -> unit) -> 'a -> unit;;
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 7adc74930e..4c59eadba8 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.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 Tacexpr
-(*i*)
 
-(* Interpretation of extended vernac phrases. *)
+(** Interpretation of extended vernac phrases. *)
 
 val disable_drop : exn -> exn
 
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
index 2f1621a7af..4c14c836ae 100644
--- a/toplevel/whelp.mli
+++ b/toplevel/whelp.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*)
 
-(* Coq interface to the Whelp query engine developed at
+(** Coq interface to the Whelp query engine developed at
    the University of Bologna *)
 
 open Names