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

16 files changed, 181 insertions, 188 deletions

diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index a45ea9549c..50132fd385 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.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 Topconstr
@@ -19,14 +18,13 @@ open Ppextend
 open Rawterm
 open Genarg
 open Mod_subst
-(*i*)
 
 (** Mapping of grammar productions to camlp4 actions
     Used for Coq-level Notation and Tactic Notation,
     and for ML-level tactic and vernac extensions
  *)
 
-(* For constr notations *)
+(** For constr notations *)
 
 type grammar_constr_prod_item =
   | GramConstrTerminal of Token.pattern
@@ -38,14 +36,14 @@ type grammar_constr_prod_item =
 type notation_grammar =
     int * Gramext.g_assoc option * notation * grammar_constr_prod_item list list
 
-(* For tactic and vernac notations *)
+(** For tactic and vernac notations *)
 
 type grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal of loc * argument_type *
       Gram.te prod_entry_key * identifier option
 
-(* Adding notations *)
+(** Adding notations *)
 
 type all_grammar_command =
   | Notation of (precedence * tolerability list) * notation_grammar
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 7643120f3c..6bf8165ebd 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.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*)
 
 open Util
 
-(**********************************************************************)
-(* General entry keys *)
+(*********************************************************************
+   General entry keys *)
 
-(* This intermediate abstract representation of entries can           *)
-(* both be reified into mlexpr for the ML extensions and              *)
-(* dynamically interpreted as entries for the Coq level extensions    *)
+(** This intermediate abstract representation of entries can           
+   both be reified into mlexpr for the ML extensions and              
+   dynamically interpreted as entries for the Coq level extensions    *)
 
 type 'a prod_entry_key =
   | Alist1 of 'a prod_entry_key
@@ -30,8 +30,8 @@ type 'a prod_entry_key =
   | Agram of 'a Gramext.g_entry
   | Aentry of string * string
 
-(**********************************************************************)
-(* Entry keys for constr notations                                    *)
+(*********************************************************************
+   Entry keys for constr notations                                    *)
 
 type side = Left | Right
 
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
index 9eff5dc132..f15c388b6c 100644
--- a/parsing/extrawit.mli
+++ b/parsing/extrawit.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*)
 
@@ -12,9 +12,9 @@ open Util
 open Genarg
 open Tacexpr
 
-(* This file defines extra argument types *)
+(** This file defines extra argument types *)
 
-(* Tactics as arguments *)
+(** Tactics as arguments *)
 
 val tactic_main_level : int
 
diff --git a/parsing/g_intsyntax.mli b/parsing/g_intsyntax.mli
index c74ae57884..40e16b83c6 100644
--- a/parsing/g_intsyntax.mli
+++ b/parsing/g_intsyntax.mli
@@ -1,13 +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 $$ i*)
 
 
-(* digit based syntax for int31 and bigint *)
+(** digit based syntax for int31 and bigint *)
diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli
index bf3921bf15..20f5c1bfd1 100644
--- a/parsing/g_natsyntax.mli
+++ b/parsing/g_natsyntax.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*)
 
-(* Nice syntax for naturals. *)
+(** Nice syntax for naturals. *)
 
 open Notation
 
diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli
index b7e6e994e5..c4f39f80b0 100644
--- a/parsing/g_zsyntax.mli
+++ b/parsing/g_zsyntax.mli
@@ -1,11 +1,11 @@
-(************************************************************************)
-(*  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*)
 
-(* Nice syntax for integers. *)
+(** Nice syntax for integers. *)
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 1b40d7f178..aabac79fb7 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.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*)
 
@@ -26,7 +26,7 @@ val is_keyword : string -> bool
 
 val location_function : int -> loc
 
-(* for coqdoc *)
+(** for coqdoc *)
 type location_table
 val location_table : unit -> location_table
 val restore_location_table : location_table -> unit
@@ -47,6 +47,6 @@ val set_xml_output_comment : (string -> unit) -> unit
 
 val terminal : string -> string * string
 
-(* The lexer of Coq *)
+(** The lexer of Coq *)
 
 val lexer : Compat.lexer
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7ed05ed5c7..f9e65acacc 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.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*)
 
@@ -18,13 +18,13 @@ open Topconstr
 open Tacexpr
 open Libnames
 
-(**********************************************************************)
-(* The parser of Coq                                                  *)
+(*********************************************************************
+   The parser of Coq                                                  *)
 
 module Gram : Grammar.S with type te = Compat.token
 
-(**********************************************************************)
-(* The parser of Coq is built from three kinds of rule declarations:
+(*********************************************************************
+   The parser of Coq is built from three kinds of rule declarations:
    - dynamic rules declared at the evaluation of Coq files (using
      e.g. Notation, Infix, or Tactic Notation)
    - static rules explicitly defined in files g_*.ml4
@@ -32,7 +32,7 @@ module Gram : Grammar.S with type te = Compat.token
      VERNAC EXTEND (see e.g. file extratactics.ml4)
 *)
 
-(* Dynamic extension of rules
+(** Dynamic extension of rules
 
     For constr notations, dynamic addition of new rules is done in
     several steps:
@@ -98,54 +98,54 @@ module Gram : Grammar.S with type te = Compat.token
 
 *)
 
-(* The superclass of all grammar entries *)
+(** The superclass of all grammar entries *)
 type grammar_object
 
 type camlp4_rule =
     Compat.token Gramext.g_symbol list * Gramext.g_action
 
 type camlp4_entry_rules =
-    (* first two parameters are name and assoc iff a level is created *)
+    (** first two parameters are name and assoc iff a level is created *)
     string option * Gramext.g_assoc option * camlp4_rule list
 
-(* Add one extension at some camlp4 position of some camlp4 entry *)
+(** Add one extension at some camlp4 position of some camlp4 entry *)
 val grammar_extend :
   grammar_object Gram.Entry.e -> Gramext.position option ->
-   (* for reinitialization if ever needed: *) Gramext.g_assoc option ->
+   (** for reinitialization if ever needed: *) Gramext.g_assoc option ->
      camlp4_entry_rules list -> unit
 
-(* Remove the last n extensions *)
+(** Remove the last n extensions *)
 val remove_grammars : int -> unit
 
 
 
 
-(* The type of typed grammar objects *)
+(** The type of typed grammar objects *)
 type typed_entry
 
-(* The possible types for extensible grammars *)
+(** The possible types for extensible grammars *)
 type entry_type = argument_type
 
 val type_of_typed_entry : typed_entry -> entry_type
 val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e
 val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e
 
-(* Temporary activate camlp4 verbosity *)
+(** Temporary activate camlp4 verbosity *)
 
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
-(* Parse a string *)
+(** Parse a string *)
 
 val parse_string : 'a Gram.Entry.e -> string -> 'a
 val eoi_entry : 'a Gram.Entry.e -> 'a Gram.Entry.e
 val map_entry : ('a -> 'b) -> 'a Gram.Entry.e -> 'b Gram.Entry.e
 
-(**********************************************************************)
-(* Table of Coq statically defined grammar entries                    *)
+(*********************************************************************
+   Table of Coq statically defined grammar entries                    *)
 
 type gram_universe
 
-(* There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
+(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *)
 
 val get_univ : string -> gram_universe
 
@@ -249,40 +249,40 @@ module Vernac_ :
     val vernac_eoi : vernac_expr Gram.Entry.e
   end
 
-(* The main entry: reads an optional vernac command *)
+(** The main entry: reads an optional vernac command *)
 val main_entry : (loc * vernac_expr) option Gram.Entry.e
 
-(**********************************************************************)
-(* Mapping formal entries into concrete ones                          *)
+(*********************************************************************
+   Mapping formal entries into concrete ones                          *)
 
-(* Binding constr entry keys to entries and symbols *)
+(** Binding constr entry keys to entries and symbols *)
 
-val interp_constr_entry_key : bool (* true for cases_pattern *) ->
+val interp_constr_entry_key : bool (** true for cases_pattern *) ->
   constr_entry_key -> grammar_object Gram.Entry.e * int option
 
 val symbol_of_constr_prod_entry_key : Gramext.g_assoc option ->
   constr_entry_key -> bool -> constr_prod_entry_key ->
     Compat.token Gramext.g_symbol
 
-(* Binding general entry keys to symbols *)
+(** Binding general entry keys to symbols *)
 
 val symbol_of_prod_entry_key :
   Gram.te prod_entry_key -> Gram.te Gramext.g_symbol
 
-(**********************************************************************)
-(* Interpret entry names of the form "ne_constr_list" as entry keys   *)
+(*********************************************************************
+   Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
-val interp_entry_name : bool (* true to fail on unknown entry *) ->
+val interp_entry_name : bool (** true to fail on unknown entry *) ->
   int option -> string -> string -> entry_type * Gram.te prod_entry_key
 
-(**********************************************************************)
-(* Registering/resetting the level of a constr entry                  *)
+(*********************************************************************
+   Registering/resetting the level of a constr entry                  *)
 
 val find_position :
-  bool (* true if for creation in pattern entry; false if in constr entry *) ->
+  bool (** true if for creation in pattern entry; false if in constr entry *) ->
   Gramext.g_assoc option -> int option ->
     Gramext.position option * Gramext.g_assoc option * string option *
-    (* for reinitialization: *) Gramext.g_assoc option
+    (** for reinitialization: *) Gramext.g_assoc option
 
 val synchronize_level_positions : unit -> unit
 
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 1aa173e249..f1bb49312f 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -1,11 +1,11 @@
 
-(************************************************************************)
-(*  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*)
 
@@ -80,7 +80,7 @@ type term_pr = {
 val set_term_pr : term_pr -> unit
 val default_term_pr : term_pr
 
-(* The modular constr printer.
+(** The modular constr printer.
     [modular_constr_pr pr s p t] prints the head of the term [t] and calls
     [pr] on its subterms.
     [s] is typically {!Pp.mt} and [p] is [lsimple] for "constr" printers and [ltop]
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 446dc9f9d4..a6eacd53a9 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.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*)
 
@@ -43,7 +43,7 @@ type 'a extra_genarg_printer =
     (tolerability -> glob_tactic_expr -> std_ppcmds) ->
     'a -> std_ppcmds
 
-  (* if the boolean is false then the extension applies only to old syntax *)
+  (** if the boolean is false then the extension applies only to old syntax *)
 val declare_extra_genarg_pprule :
   ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) ->
   ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) ->
@@ -51,7 +51,7 @@ val declare_extra_genarg_pprule :
 
 type grammar_terminals = string option list
 
-  (* if the boolean is false then the extension applies only to old syntax *)
+  (** if the boolean is false then the extension applies only to old syntax *)
 val declare_extra_tactic_pprule :
   string * argument_type list * (int * grammar_terminals) -> unit
 
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli
index c24744f300..6c2916f412 100644
--- a/parsing/ppvernac.mli
+++ b/parsing/ppvernac.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/parsing/prettyp.mli b/parsing/prettyp.mli
index ba1977e893..04aad9ab42 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.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 Util
 open Names
@@ -19,9 +18,8 @@ open Reductionops
 open Libnames
 open Nametab
 open Genarg
-(*i*)
 
-(* A Pretty-Printer for the Calculus of Inductive Constructions. *)
+(** A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
 val assumptions_for_print : name list -> Termops.names_context
 
@@ -38,7 +36,8 @@ val print_judgment : env -> unsafe_judgment -> std_ppcmds
 val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds
 val print_eval :
   reduction_function -> env -> Evd.evar_map -> Topconstr.constr_expr -> unsafe_judgment -> std_ppcmds
-(* This function is exported for the graphical user-interface pcoq *)
+
+(** This function is exported for the graphical user-interface pcoq *)
 val build_inductive : mutual_inductive -> int ->
   global_reference * rel_context * types * identifier array * types array
 val print_name : reference or_by_notation -> std_ppcmds
@@ -52,21 +51,21 @@ val print_extraction : unit -> std_ppcmds
 val print_extracted_vars : unit -> std_ppcmds
 i*)
 
-(* Pretty-printing functions for classes and coercions *)
+(** Pretty-printing functions for classes and coercions *)
 val print_graph : unit -> std_ppcmds
 val print_classes : unit -> std_ppcmds
 val print_coercions : unit -> std_ppcmds
 val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds
 val print_canonical_projections : unit -> std_ppcmds
 
-(* Pretty-printing functions for type classes and instances *)
+(** Pretty-printing functions for type classes and instances *)
 val print_typeclasses : unit -> std_ppcmds
 val print_instances : global_reference -> std_ppcmds
 val print_all_instances : unit -> std_ppcmds
 
 val inspect : int -> std_ppcmds
 
-(* Locate *)
+(** Locate *)
 val print_located_qualid : reference -> std_ppcmds
 
 type object_pr = {
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 2c1586abf7..6289fa66a7 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.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 Libnames
@@ -23,11 +22,10 @@ open Evd
 open Proof_type
 open Rawterm
 open Tacexpr
-(*i*)
 
-(* These are the entry points for printing terms, context, tac, ... *)
+(** These are the entry points for printing terms, context, tac, ... *)
 
-(* Terms *)
+(** Terms *)
 
 val pr_lconstr_env         : env -> constr -> std_ppcmds
 val pr_lconstr_env_at_top  : env -> constr -> std_ppcmds
@@ -68,7 +66,7 @@ val pr_cases_pattern       : cases_pattern -> std_ppcmds
 
 val pr_sort                : sorts -> std_ppcmds
 
-(* Printing global references using names as short as possible *)
+(** Printing global references using names as short as possible *)
 
 val pr_global_env          : Idset.t -> global_reference -> std_ppcmds
 val pr_global              : global_reference -> std_ppcmds
@@ -79,7 +77,7 @@ val pr_constructor         : env -> constructor -> std_ppcmds
 val pr_inductive           : env -> inductive -> std_ppcmds
 val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds
 
-(* Contexts *)
+(** Contexts *)
 
 val pr_ne_context_of       : std_ppcmds -> env -> std_ppcmds
 
@@ -92,14 +90,14 @@ val pr_rel_context         : env -> rel_context -> std_ppcmds
 val pr_rel_context_of      : env -> std_ppcmds
 val pr_context_of          : env -> std_ppcmds
 
-(* Predicates *)
+(** Predicates *)
 
 val pr_predicate           : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds
 val pr_cpred               : Cpred.t -> std_ppcmds
 val pr_idpred              : Idpred.t -> std_ppcmds
 val pr_transparent_state   : transparent_state -> std_ppcmds
 
-(* Proofs *)
+(** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
 val pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds
@@ -111,19 +109,19 @@ val pr_evars_int           : int -> (evar * evar_info) list -> std_ppcmds
 
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
-(* Emacs/proof general support *)
-(* (emacs_str s alts) outputs
+(** Emacs/proof general support 
+   (emacs_str s alts) outputs
    - s if emacs mode & unicode allowed,
    - alts if emacs mode and & unicode not allowed
    - nothing otherwise *)
 val emacs_str              : string -> string -> string
 
-(* Backwards compatibility *)
+(** Backwards compatibility *)
 
-val prterm                 : constr -> std_ppcmds (* = pr_lconstr *)
+val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 
 
-(* spiwack: printer function for sets of Environ.assumption.
+(** spiwack: printer function for sets of Environ.assumption.
             It is used primarily by the Print Assumption command. *)
 val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds
 
diff --git a/parsing/printmod.mli b/parsing/printmod.mli
index a3a16e8ecb..b7926543d6 100644
--- a/parsing/printmod.mli
+++ b/parsing/printmod.mli
@@ -1,15 +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        
+  ***********************************************************************)
 
 open Pp
 open Names
 
-(* false iff the module is an element of an open module type *)
+(** false iff the module is an element of an open module type *)
 val printable_body : dir_path -> bool
 
 val print_module : bool -> module_path -> std_ppcmds
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index 7c0fec9a2a..4fe853702a 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.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/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index 96cbeb9a84..836c4712ba 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -1,22 +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*)
 
-(*i*)
 open Pp
 open Sign
 open Evd
 open Tacexpr
 open Proof_type
-(*i*)
 
-(* These are the entry points for tactics, proof trees, ... *)
+(** These are the entry points for tactics, proof trees, ... *)
 
 val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
 val pr_rule     : rule -> std_ppcmds