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

22 files changed, 319 insertions, 345 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 072e02989..37fe3d441 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.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
@@ -22,29 +21,28 @@ open Evd
 open Libnames
 open Vernacexpr
 open Mod_subst
-(*i*)
 
 type auto_tactic =
-  | Res_pf     of constr * clausenv    (* Hint Apply *)
-  | ERes_pf    of constr * clausenv    (* Hint EApply *)
+  | Res_pf     of constr * clausenv    (** Hint Apply *)
+  | ERes_pf    of constr * clausenv    (** Hint EApply *)
   | Give_exact of constr
-  | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *)
-  | Unfold_nth of evaluable_global_reference          (* Hint Unfold *)
-  | Extern     of Tacexpr.glob_tactic_expr   (* Hint Extern *)
+  | Res_pf_THEN_trivial_fail of constr * clausenv (** Hint Immediate *)
+  | Unfold_nth of evaluable_global_reference          (** Hint Unfold *)
+  | Extern     of Tacexpr.glob_tactic_expr   (** Hint Extern *)
 
 open Rawterm
 
 type pri_auto_tactic = {
-  pri   : int;            (* A number between 0 and 4, 4 = lower priority *)
-  pat   : constr_pattern option; (* A pattern for the concl of the Goal *)
-  code  : auto_tactic;    (* the tactic to apply when the concl matches pat *)
+  pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
+  pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
+  code  : auto_tactic;    (** the tactic to apply when the concl matches pat *)
 }
 
 type stored_data = pri_auto_tactic
 
 type search_entry
 
-(* The head may not be bound. *)
+(** The head may not be bound. *)
 
 type hint_entry = global_reference option * pri_auto_tactic
 
@@ -85,7 +83,7 @@ val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
 
-(* [create_hint_db local name st use_dn].
+(** [create_hint_db local name st use_dn].
    [st] is a transparency state for unification using this db
    [use_dn] switches the use of the discrimination net for all hints
    and patterns. *)
@@ -108,13 +106,13 @@ val print_hint_db_by_name : hint_db_name -> unit
 
 val print_hint_db : Hint_db.t -> unit
 
-(* [make_exact_entry pri (c, ctyp)].
+(** [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c]. *)
 
 val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
 
-(* [make_apply_entry (eapply,verbose) pri (c,cty)].
+(** [make_apply_entry (eapply,verbose) pri (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
    [hnf] should be true if we should expand the head of cty before searching for
    products;
@@ -125,7 +123,7 @@ val make_apply_entry :
   env -> evar_map -> bool * bool * bool -> int option -> constr * constr
       -> hint_entry
 
-(* A constr which is Hint'ed will be:
+(** A constr which is Hint'ed will be:
    (1) used as an Exact, if it does not start with a product
    (2) used as an Apply, if its HNF starts with a product, and
        has no missing arguments.
@@ -136,7 +134,7 @@ val make_resolves :
   env -> evar_map -> bool * bool * bool -> int option -> constr ->
       hint_entry list
 
-(* [make_resolve_hyp hname htyp].
+(** [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
    Never raises a user exception;
    If the hyp cannot be used as a Hint, the empty list is returned. *)
@@ -144,7 +142,7 @@ val make_resolves :
 val make_resolve_hyp :
   env -> evar_map -> named_declaration -> hint_entry list
 
-(* [make_extern pri pattern tactic_expr] *)
+(** [make_extern pri pattern tactic_expr] *)
 
 val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
@@ -161,7 +159,7 @@ val set_extern_subst_tactic :
   (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr)
   -> unit
 
-(* Create a Hint database from the pairs (name, constr).
+(** Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
 
@@ -173,47 +171,47 @@ val default_search_depth : int ref
 
 val auto_unif_flags : Unification.unify_flags
 
-(* Try unification with the precompiled clause, then use registered Apply *)
+(** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve_nodelta : (constr * clausenv) -> tactic
 
 val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic
 
-(* [ConclPattern concl pat tacast]:
+(** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
 val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> tactic
 
-(* The Auto tactic *)
+(** The Auto tactic *)
 
 val auto : int -> constr list -> hint_db_name list -> tactic
 
-(* Auto with more delta. *)
+(** Auto with more delta. *)
 
 val new_auto : int -> constr list -> hint_db_name list -> tactic
 
-(* auto with default search depth and with the hint database "core" *)
+(** auto with default search depth and with the hint database "core" *)
 val default_auto : tactic
 
-(* auto with all hint databases except the "v62" compatibility database *)
+(** auto with all hint databases except the "v62" compatibility database *)
 val full_auto : int -> constr list -> tactic
 
-(* auto with all hint databases except the "v62" compatibility database
+(** auto with all hint databases except the "v62" compatibility database
    and doing delta *)
 val new_full_auto : int -> constr list -> tactic
 
-(* auto with default search depth and with all hint databases
+(** auto with default search depth and with all hint databases
    except the "v62" compatibility database *)
 val default_full_auto : tactic
 
-(* The generic form of auto (second arg [None] means all bases) *)
+(** The generic form of auto (second arg [None] means all bases) *)
 val gen_auto : int option -> constr list -> hint_db_name list option -> tactic
 
-(* The hidden version of auto *)
+(** The hidden version of auto *)
 val h_auto   : int option -> constr list -> hint_db_name list option -> tactic
 
-(* Trivial *)
+(** Trivial *)
 val trivial : constr list -> hint_db_name list -> tactic
 val gen_trivial : constr list -> hint_db_name list option -> tactic
 val full_trivial : constr list -> tactic
@@ -221,15 +219,16 @@ val h_trivial : constr list -> hint_db_name list option -> tactic
 
 val pr_autotactic : auto_tactic -> Pp.std_ppcmds
 
-(*s The following is not yet up to date -- Papageno. *)
+(** {6 The following is not yet up to date -- Papageno. } *)
 
-(* DAuto *)
+(** DAuto *)
 val dauto : int option * int option -> constr list -> tactic
 val default_search_decomp : int ref
 val default_dauto : tactic
 
 val h_dauto : int option * int option -> constr list -> tactic
-(* SuperAuto *)
+
+(** SuperAuto *)
 
 type autoArguments =
   | UsingTDB
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index cf0d58ccb..a9556891a 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -1,34 +1,32 @@
-(************************************************************************)
-(*  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 Term
 open Tacexpr
 open Tacmach
 open Equality
-(*i*)
 
-(* Rewriting rules before tactic interpretation *)
+(** Rewriting rules before tactic interpretation *)
 type raw_rew_rule = Util.loc * Term.constr * bool * Tacexpr.raw_tactic_expr
 
-(* To add rewriting rules to a base *)
+(** To add rewriting rules to a base *)
 val add_rew_rules : string -> raw_rew_rule list -> unit
 
-(* The AutoRewrite tactic.
+(** The AutoRewrite tactic.
    The optional conditions tell rewrite how to handle matching and side-condition solving.
    Default is Naive: first match in the clause, don't look at the side-conditions to
    tell if the rewrite succeeded. *)
 val autorewrite : ?conds:conditions -> tactic -> string list -> tactic
 val autorewrite_in : ?conds:conditions -> Names.identifier -> tactic -> string list -> tactic
 
-(* Rewriting rules *)
+(** Rewriting rules *)
 type rew_rule = { rew_lemma: constr;
 		  rew_type: types;
 		  rew_pat: constr;
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index ebded23ac..ebb046a05 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(*  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 Term
 open Pattern
 open Names
-(*i*)
 
-(* Discrimination nets with bounded depth. *)
+(** Discrimination nets with bounded depth. *)
 module Make :
   functor (Z : Map.OrderedType) ->
 sig
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 9c38362a8..b5fdf5a1b 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(*  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 Proof_type
 open Rawterm
 open Genarg
-(*i*)
 
 val absurd                      : constr -> tactic
 val contradiction               : constr with_bindings option -> tactic
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index 41fd497f7..465a2a377 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(*  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 Tacmach
 open Tacexpr
-(*i*)
 
-(* Programmable destruction of hypotheses and conclusions. *)
+(** Programmable destruction of hypotheses and conclusions. *)
 
 val set_extern_interp : (glob_tactic_expr -> tactic) -> unit
 
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 3cb52a565..662ac19af 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -17,7 +17,7 @@ sig
 
   val create : unit -> t
     
-  (* [add t f (tree,inf)] adds a structured object [tree] together with
+  (** [add t f (tree,inf)] adds a structured object [tree] together with
      the associated information [inf] to the table [t]; the function
      [f] is used to translated [tree] into its prefix decomposition: [f]
      must decompose any tree into a label characterizing its root node and
@@ -31,7 +31,8 @@ sig
       
   type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res
     
-(* [lookup t f tree] looks for trees (and their associated
+
+(** [lookup t f tree] looks for trees (and their associated
    information) in table [t] such that the structured object [tree]
    matches against them; [f] is used to translated [tree] into its
    prefix decomposition: [f] must decompose any tree into a label
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index a5d1f0d37..595917bdf 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -1,12 +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        *)
-(************************************************************************)
-
-(*i*)
+(***********************************************************************
+    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 Proof_type
 open Tacexpr
@@ -15,7 +14,6 @@ open Topconstr
 open Evd
 open Environ
 open Explore
-(*i*)
 
 val hintbases : hint_db_name list option Pcoq.Gram.Entry.e
 val wit_hintbases : hint_db_name list option typed_abstract_argument_type
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 25ae07000..7fbb16ba1 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -1,23 +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*)
 
-(*i*)
 open Names
 open Term
 open Proof_type
 open Tacmach
 open Genarg
 open Tacticals
-(*i*)
 
-(* Eliminations tactics. *)
+(** Eliminations tactics. *)
 
 val introElimAssumsThen :
   (branch_assumptions -> tactic) -> branch_args -> tactic
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index fecf3e60d..ef1c4ec3e 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -1,16 +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        
+  ***********************************************************************)
 
-(* $Id$ *)
+(** {% $ %}Id: elimschemes.mli 12584 2009-12-13 21:04:34Z herbelin {% $ %} *)
 
 open Ind_tables
 
-(* Induction/recursion schemes *)
+(** Induction/recursion schemes *)
 
 val rect_scheme_kind_from_prop : individual scheme_kind
 val ind_scheme_kind_from_prop : individual scheme_kind
@@ -20,7 +20,7 @@ val ind_dep_scheme_kind_from_type : individual scheme_kind
 val rec_dep_scheme_kind_from_type : individual scheme_kind
 
 
-(* Case analysis schemes *)
+(** Case analysis schemes *)
 
 val case_scheme_kind_from_type : individual scheme_kind
 val case_scheme_kind_from_prop : individual scheme_kind
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index a6ffe9e21..bdf3bbe76 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.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*)
 
-(* This file builds schemes relative to equality inductive types *)
+(** This file builds schemes relative to equality inductive types *)
 
 open Names
 open Term
 open Environ
 open Ind_tables
 
-(* Builds a left-to-right rewriting scheme for an equality type *)
+(** Builds a left-to-right rewriting scheme for an equality type *)
 
 val rew_l2r_dep_scheme_kind : individual scheme_kind
 val rew_l2r_scheme_kind : individual scheme_kind
@@ -32,7 +32,7 @@ val build_l2r_forward_rew_scheme :
 val build_r2l_forward_rew_scheme :
   bool -> env -> inductive -> sorts_family -> constr
 
-(* Builds a symmetry scheme for a symmetrical equality type *)
+(** Builds a symmetry scheme for a symmetrical equality type *)
 
 val build_sym_scheme : env -> inductive -> constr
 val sym_scheme_kind : individual scheme_kind
@@ -40,7 +40,7 @@ val sym_scheme_kind : individual scheme_kind
 val build_sym_involutive_scheme : env -> inductive -> constr
 val sym_involutive_scheme_kind : individual scheme_kind
 
-(* Builds a congruence scheme for an equality type *)
+(** Builds a congruence scheme for an equality type *)
 
 val congr_scheme_kind : individual scheme_kind
 val build_congr : env -> constr * constr -> inductive -> constr
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 2e30cdfbe..0cf4dbb80 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.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/tactics/extraargs.mli b/tactics/extraargs.mli
index 4492fd842..3421ded92 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.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*)
 
@@ -51,7 +51,7 @@ val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type
 
 
 
-(* Spiwack: Primitive for retroknowledge registration *)
+(** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e
 val rawwit_retroknowledge_field :  Retroknowledge.field raw_abstract_argument_type
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 82006f602..259fe8814 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.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/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 36b0830dd..dae0281bd 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -1,15 +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*)
 
-(*i*)
 open Names
 open Util
 open Term
@@ -21,12 +20,11 @@ open Rawterm
 open Evd
 open Clenv
 open Termops
-(*i*)
 
-(* Tactics for the interpreter. They left a trace in the proof tree
+(** Tactics for the interpreter. They left a trace in the proof tree
    when they are called. *)
 
-(* Basic tactics *)
+(** Basic tactics *)
 
 val h_intro_move      : identifier option -> identifier move_location -> tactic
 val h_intro           : identifier -> tactic
@@ -63,7 +61,7 @@ val h_generalize_dep  : constr -> tactic
 val h_let_tac         : letin_flag -> name -> constr ->
                         Tacticals.clause -> tactic
 
-(* Derived basic tactics *)
+(** Derived basic tactics *)
 
 val h_simple_induction   : quantified_hypothesis -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
@@ -84,17 +82,17 @@ val h_induction_destruct : rec_flag -> evars_flag ->
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
-(* Automation tactic : see Auto *)
+(** Automation tactic : see Auto *)
 
 
-(* Context management *)
+(** Context management *)
 val h_clear           : bool -> identifier list -> tactic
 val h_clear_body      : identifier list -> tactic
 val h_move            : bool -> identifier -> identifier move_location -> tactic
 val h_rename          : (identifier*identifier) list -> tactic
 val h_revert          : identifier list -> tactic
 
-(* Constructors *)
+(** Constructors *)
 val h_constructor     : evars_flag -> int -> constr bindings -> tactic
 val h_left            : evars_flag -> constr bindings -> tactic
 val h_right           : evars_flag -> constr bindings -> tactic
@@ -105,12 +103,12 @@ val h_simplest_left   : tactic
 val h_simplest_right  : tactic
 
 
-(* Conversion *)
+(** Conversion *)
 val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
 val h_change          :
   Pattern.constr_pattern option -> constr -> Tacticals.clause -> tactic
 
-(* Equivalence relations *)
+(** Equivalence relations *)
 val h_reflexivity     : tactic
 val h_symmetry        : Tacticals.clause -> tactic
 val h_transitivity    : constr option -> tactic
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 9b04a2cd2..40ad0da9b 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.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
@@ -16,9 +15,9 @@ open Sign
 open Evd
 open Pattern
 open Coqlib
-(*i*)
 
-(*s Given a term with second-order variables in it,
+(** {6 Sect } *)
+(** Given a term with second-order variables in it,
    represented by Meta's, and possibly applied using SoApp
    terms, this function will perform second-order, binding-preserving,
    matching, in the case where the pattern is a pattern in the sense
@@ -37,7 +36,8 @@ open Coqlib
    intersection of the free-rels of the term and the current stack be
    contained in the arguments of the application *)
 
-(*s I implemented the following functions which test whether a term [t]
+(** {6 Sect } *)
+(** I implemented the following functions which test whether a term [t]
    is an inductive but non-recursive type, a general conjuction, a
    general disjunction, or a type with no constructors.
 
@@ -52,36 +52,36 @@ type testing_function = constr -> bool
 val match_with_non_recursive_type : (constr * constr list) matching_function
 val is_non_recursive_type         : testing_function
 
-(* Non recursive type with no indices and exactly one argument for each
+(** Non recursive type with no indices and exactly one argument for each
    constructor; canonical definition of n-ary disjunction if strict *)
 val match_with_disjunction : ?strict:bool -> (constr * constr list) matching_function
 val is_disjunction         : ?strict:bool -> testing_function
 
-(* Non recursive tuple (one constructor and no indices) with no inner
+(** Non recursive tuple (one constructor and no indices) with no inner
    dependencies; canonical definition of n-ary conjunction if strict *)
 val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function
 val is_conjunction         : ?strict:bool -> testing_function
 
-(* Non recursive tuple, possibly with inner dependencies *)
+(** Non recursive tuple, possibly with inner dependencies *)
 val match_with_record      : (constr * constr list) matching_function
 val is_record              : testing_function
 
-(* Like record but supports and tells if recursive (e.g. Acc) *)
+(** Like record but supports and tells if recursive (e.g. Acc) *)
 val match_with_tuple       : (constr * constr list * bool) matching_function
 val is_tuple               : testing_function
 
-(* No constructor, possibly with indices *)
+(** No constructor, possibly with indices *)
 val match_with_empty_type  : constr matching_function
 val is_empty_type          : testing_function
 
-(* type with only one constructor and no arguments, possibly with indices *)
+(** type with only one constructor and no arguments, possibly with indices *)
 val match_with_unit_or_eq_type : constr matching_function
 val is_unit_or_eq_type     : testing_function
 
-(* type with only one constructor and no arguments, no indices *)
+(** type with only one constructor and no arguments, no indices *)
 val is_unit_type           : testing_function
 
-(* type with only one constructor, no arguments and at least one dependency *)
+(** type with only one constructor, no arguments and at least one dependency *)
 val is_inductive_equality  : inductive -> bool
 val match_with_equality_type : (constr * constr list) matching_function
 val is_equality_type       : testing_function
@@ -95,7 +95,7 @@ val is_forall_term            : testing_function
 val match_with_imp_term    : (constr * constr) matching_function
 val is_imp_term            : testing_function
 
-(* I added these functions to test whether a type contains dependent
+(** I added these functions to test whether a type contains dependent
   products or not, and if an inductive has constructors with dependent types
  (excluding parameters). this is useful to check whether a conjunction is a
  real conjunction and not a dependent tuple. (Pierre Corbineau, 13/5/2002) *)
@@ -109,7 +109,7 @@ val is_nodep_ind           : testing_function
 val match_with_sigma_type   : (constr * constr list) matching_function
 val is_sigma_type           : testing_function
 
-(* Recongnize inductive relation defined by reflexivity *)
+(** Recongnize inductive relation defined by reflexivity *)
 
 type equation_kind =
   | MonomorphicLeibnizEq of constr * constr
@@ -123,37 +123,37 @@ val match_with_equation:
 
 (***** Destructing patterns bound to some theory *)
 
-(* Match terms [eq A t u], [identity A t u] or [JMeq A t A u] *)
-(* Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
+(** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] 
+   Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
 val find_eq_data_decompose : Proof_type.goal sigma -> constr ->
       coq_eq_data * (types * constr * constr)
 
-(* Idem but fails with an error message instead of PatternMatchingFailure *)
+(** Idem but fails with an error message instead of PatternMatchingFailure *)
 val find_this_eq_data_decompose : Proof_type.goal sigma -> constr ->
       coq_eq_data * (types * constr * constr)
 
-(* A variant that returns more informative structure on the equality found *)
+(** A variant that returns more informative structure on the equality found *)
 val find_eq_data : constr -> coq_eq_data * equation_kind
 
-(* Match a term of the form [(existT A P t p)] *)
-(* Returns associated lemmas and [A,P,t,p] *)
+(** Match a term of the form [(existT A P t p)] 
+   Returns associated lemmas and [A,P,t,p] *)
 val find_sigma_data_decompose : constr ->
   coq_sigma_data * (constr * constr * constr * constr)
 
-(* Match a term of the form [{x:A|P}], returns [A] and [P] *)
+(** Match a term of the form [{x:A|P}], returns [A] and [P] *)
 val match_sigma : constr -> constr * constr
 
 val is_matching_sigma : constr -> bool
 
-(* Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
+(** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
    [t,u,T] and a boolean telling if equality is on the left side *)
 val match_eqdec : constr -> bool * constr * constr * constr * constr
 
-(* Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
+(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
 open Proof_type
 open Tacmach
 val dest_nf_eq : goal sigma -> constr -> (constr * constr * constr)
 
-(* Match a negation *)
+(** Match a negation *)
 val is_matching_not : constr -> bool
 val is_matching_imp_False : constr -> bool
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 8ec0e2db2..a7780206b 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.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
@@ -16,7 +15,6 @@ open Tacmach
 open Genarg
 open Tacexpr
 open Rawterm
-(*i*)
 
 type inversion_status = Dep of constr option | NoDep
 
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 027ea5734..3f866d5da 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(*  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 Term
 open Pattern
 open Libnames
-(*i*)
 
-(* Named, bounded-depth, term-discrimination nets. *)
+(** Named, bounded-depth, term-discrimination nets. *)
 module Make :
   functor (Y:Map.OrderedType) ->
 sig
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 89e531675..c9a4598e5 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.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/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 71ee29f8c..771d28fba 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.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
@@ -21,9 +20,8 @@ open Genarg
 open Topconstr
 open Mod_subst
 open Redexpr
-(*i*)
 
-(* Values for interpretation *)
+(** Values for interpretation *)
 type value =
   | VRTactic of (goal list sigma)
   | VFun of ltac_trace * (identifier*value) list *
@@ -36,7 +34,7 @@ type value =
   | VList of value list
   | VRec of (identifier*value) list ref * glob_tactic_expr
 
-(* Signature for interpretation: val\_interp and interpretation functions *)
+(** Signature for interpretation: val\_interp and interpretation functions *)
 and interp_sign =
   { lfun : (identifier * value) list;
     avoid_ids : identifier list;
@@ -46,10 +44,10 @@ and interp_sign =
 val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env ->
   Pretyping.var_map * Pretyping.unbound_ltac_var_map
 
-(* Transforms an id into a constr if possible *)
+(** Transforms an id into a constr if possible *)
 val constr_of_id : Environ.env -> identifier -> constr
 
-(* To embed several objects in Coqast.t *)
+(** To embed several objects in Coqast.t *)
 val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t
 val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)
 
@@ -58,19 +56,19 @@ val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr
 val valueIn : value -> raw_tactic_arg
 val constrIn : constr -> constr_expr
 
-(* Sets the debugger mode *)
+(** Sets the debugger mode *)
 val set_debug : debug_info -> unit
 
-(* Gives the state of debug *)
+(** Gives the state of debug *)
 val get_debug : unit -> debug_info
 
-(* Adds a definition for tactics in the table *)
+(** Adds a definition for tactics in the table *)
 val add_tacdef :
   Vernacexpr.locality_flag -> bool ->
   (Libnames.reference * bool * raw_tactic_expr) list -> unit
 val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
-(* Tactic extensions *)
+(** Tactic extensions *)
 val add_tactic :
   string -> (typed_generic_argument list -> tactic) -> unit
 val overwriting_add_tactic :
@@ -78,7 +76,7 @@ val overwriting_add_tactic :
 val lookup_tactic :
   string -> (typed_generic_argument list) -> tactic
 
-(* Adds an interpretation function for extra generic arguments *)
+(** Adds an interpretation function for extra generic arguments *)
 type glob_sign = {
   ltacvars : identifier list * identifier list;
   ltacrecvars : (identifier * Nametab.ltac_constant) list;
@@ -118,17 +116,17 @@ val subst_genarg :
 val subst_rawconstr_and_expr :
   substitution -> rawconstr_and_expr -> rawconstr_and_expr
 
-(* Interprets any expression *)
+(** Interprets any expression *)
 val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value
 
-(* Interprets an expression that evaluates to a constr *)
+(** Interprets an expression that evaluates to a constr *)
 val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr ->
   constr
 
-(* Interprets redexp arguments *)
+(** Interprets redexp arguments *)
 val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr
 
-(* Interprets tactic expressions *)
+(** Interprets tactic expressions *)
 val interp_tac_gen : (identifier * value) list -> identifier list ->
                  debug_info -> raw_tactic_expr -> tactic
 
@@ -136,7 +134,7 @@ val interp_hyp :  interp_sign -> goal sigma -> identifier located -> identifier
 
 val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> rawconstr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings
 
-(* Initial call for interpretation *)
+(** Initial call for interpretation *)
 val glob_tactic : raw_tactic_expr -> glob_tactic_expr
 
 val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
@@ -149,21 +147,21 @@ val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr
 
 val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
 
-(* Hides interpretation for pretty-print *)
+(** Hides interpretation for pretty-print *)
 
 val hide_interp : raw_tactic_expr -> tactic option -> tactic
 
-(* Declare the default tactic to fill implicit arguments *)
+(** Declare the default tactic to fill implicit arguments *)
 val declare_implicit_tactic : tactic -> unit
 
-(* Declare the xml printer *)
+(** Declare the xml printer *)
 val declare_xml_printer :
   (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit
 
-(* printing *)
+(** printing *)
 val print_ltac : Libnames.qualid -> std_ppcmds
 
-(* Internals that can be useful for syntax extensions. *)
+(** Internals that can be useful for syntax extensions. *)
 
 exception CannotCoerceTo of string
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3dd73c92c..c357451a2 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.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
@@ -23,9 +22,8 @@ open Genarg
 open Tacexpr
 open Termops
 open Rawterm
-(*i*)
 
-(* Tacticals i.e. functions from tactics to tactics. *)
+(** Tacticals i.e. functions from tactics to tactics. *)
 
 val tclNORMEVAR      : tactic
 val tclIDTAC         : tactic
@@ -68,7 +66,7 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
 val tclFIRST_PROGRESS_ON : ('a -> tactic) -> 'a list -> tactic
 
-(*s Tacticals applying to hypotheses *)
+(** {6 Tacticals applying to hypotheses } *)
 
 val onNthHypId       : int -> (identifier -> tactic) -> tactic
 val onNthHyp         : int -> (constr -> tactic) -> tactic
@@ -96,14 +94,14 @@ val ifOnHyp     : (identifier * types -> bool) ->
 val onHyps      : (goal sigma -> named_context) ->
                   (named_context -> tactic) -> tactic
 
-(*s Tacticals applying to goal components *)
+(** {6 Tacticals applying to goal components } *)
 
-(* A [simple_clause] is a set of hypotheses, possibly extended with
+(** A [simple_clause] is a set of hypotheses, possibly extended with
    the conclusion (conclusion is represented by None) *)
 
 type simple_clause = identifier option list
 
-(* A [clause] denotes occurrences and hypotheses in a
+(** A [clause] denotes occurrences and hypotheses in a
    goal; in particular, it can abstractly refer to the set of
    hypotheses independently of the effective contents of the current goal *)
 
@@ -126,21 +124,21 @@ val onAllHypsAndConclLR : (identifier option -> tactic) -> tactic
 val onClause   : (identifier option -> tactic) -> clause -> tactic
 val onClauseLR : (identifier option -> tactic) -> clause -> tactic
 
-(*s An intermediate form of occurrence clause with no mention of occurrences *)
+(** {6 An intermediate form of occurrence clause with no mention of occurrences } *)
 
-(* A [hyp_location] is an hypothesis together with a position, in
+(** A [hyp_location] is an hypothesis together with a position, in
    body if any, in type or in both *)
 
 type hyp_location = identifier * hyp_location_flag
 
-(* A [goal_location] is either an hypothesis (together with a position, in
+(** A [goal_location] is either an hypothesis (together with a position, in
    body if any, in type or in both) or the goal *)
 
 type goal_location = hyp_location option
 
-(*s A concrete view of occurrence clauses *)
+(** {6 A concrete view of occurrence clauses } *)
 
-(* [clause_atom] refers either to an hypothesis location (i.e. an
+(** [clause_atom] refers either to an hypothesis location (i.e. an
    hypothesis with occurrences and a position, in body if any, in type
    or in both) or to some occurrences of the conclusion *)
 
@@ -148,40 +146,40 @@ type clause_atom =
   | OnHyp of identifier * occurrences_expr * hyp_location_flag
   | OnConcl of occurrences_expr
 
-(* A [concrete_clause] is an effective collection of
+(** A [concrete_clause] is an effective collection of
   occurrences in the hypotheses and the conclusion *)
 
 type concrete_clause = clause_atom list
 
-(* This interprets an [clause] in a given [goal] context *)
+(** This interprets an [clause] in a given [goal] context *)
 val concrete_clause_of : clause -> goal sigma -> concrete_clause
 
-(*s Elimination tacticals. *)
+(** {6 Elimination tacticals. } *)
 
 type branch_args = {
-  ity        : inductive;   (* the type we were eliminating on *)
-  largs      : constr list; (* its arguments *)
-  branchnum  : int;         (* the branch number *)
-  pred       : constr;      (* the predicate we used *)
-  nassums    : int;         (* the number of assumptions to be introduced *)
-  branchsign : bool list;   (* the signature of the branch.
+  ity        : inductive;   (** the type we were eliminating on *)
+  largs      : constr list; (** its arguments *)
+  branchnum  : int;         (** the branch number *)
+  pred       : constr;      (** the predicate we used *)
+  nassums    : int;         (** the number of assumptions to be introduced *)
+  branchsign : bool list;   (** the signature of the branch.
                                true=recursive argument, false=constant *)
   branchnames : intro_pattern_expr located list}
 
 type branch_assumptions = {
-  ba        : branch_args;     (* the branch args *)
-  assums    : named_context}   (* the list of assumptions introduced *)
+  ba        : branch_args;     (** the branch args *)
+  assums    : named_context}   (** the list of assumptions introduced *)
 
-(* [check_disjunctive_pattern_size loc pats n] returns an appropriate *)
-(* error message if |pats| <> n *)
+(** [check_disjunctive_pattern_size loc pats n] returns an appropriate 
+   error message if |pats| <> n *)
 val check_or_and_pattern_size :
   Util.loc -> or_and_intro_pattern_expr -> int -> unit
 
-(* Tolerate "[]" to mean a disjunctive pattern of any length *)
+(** Tolerate "[]" to mean a disjunctive pattern of any length *)
 val fix_empty_or_and_pattern : int -> or_and_intro_pattern_expr ->
   or_and_intro_pattern_expr
 
-(* Useful for [as intro_pattern] modifier *)
+(** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
   int -> intro_pattern_expr located option ->
     intro_pattern_expr located list array
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0e552bd40..2d7c07402 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.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
@@ -29,11 +28,10 @@ open Nametab
 open Rawterm
 open Pattern
 open Termops
-(*i*)
 
-(* Main tactics. *)
+(** Main tactics. *)
 
-(*s General functions. *)
+(** {6 General functions. } *)
 
 val string_of_inductive : constr -> string
 val head_constr       : constr -> constr * constr list
@@ -42,7 +40,7 @@ val is_quantified_hypothesis : identifier -> goal sigma -> bool
 
 exception Bound
 
-(*s Primitive tactics. *)
+(** {6 Primitive tactics. } *)
 
 val introduction    : identifier -> tactic
 val refine          : constr -> tactic
@@ -55,7 +53,7 @@ val fix             : identifier option -> int -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> int -> tactic
 val cofix           : identifier option -> tactic
 
-(*s Introduction tactics. *)
+(** {6 Introduction tactics. } *)
 
 val fresh_id_in_env : identifier list -> identifier -> env -> identifier
 val fresh_id : identifier list -> identifier -> goal sigma -> identifier
@@ -65,7 +63,7 @@ val intro                : tactic
 val introf               : tactic
 val intro_move        : identifier option -> identifier move_location -> tactic
 
-  (* [intro_avoiding idl] acts as intro but prevents the new identifier
+  (** [intro_avoiding idl] acts as intro but prevents the new identifier
      to belong to [idl] *)
 val intro_avoiding       : identifier list -> tactic
 
@@ -78,7 +76,7 @@ val intros_replacing     : identifier list -> tactic
 
 val intros               : tactic
 
-(* [depth_of_quantified_hypothesis b h g] returns the index of [h] in
+(** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
    the conclusion of goal [g], up to head-reduction if [b] is [true] *)
 val depth_of_quantified_hypothesis :
   bool -> quantified_hypothesis -> goal sigma -> int
@@ -88,7 +86,7 @@ val intros_until         : quantified_hypothesis -> tactic
 
 val intros_clearing      : bool list -> tactic
 
-(* Assuming a tactic [tac] depending on an hypothesis identifier,
+(** Assuming a tactic [tac] depending on an hypothesis identifier,
    [try_intros_until tac arg] first assumes that arg denotes a
    quantified hypothesis (denoted by name or by index) and try to
    introduce it in context before to apply [tac], otherwise assume the
@@ -97,21 +95,21 @@ val intros_clearing      : bool list -> tactic
 val try_intros_until :
   (identifier -> tactic) -> quantified_hypothesis -> tactic
 
-(* Apply a tactic on a quantified hypothesis, an hypothesis in context
+(** Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
 val onInductionArg :
   (constr with_bindings -> tactic) ->
     constr with_bindings induction_arg -> tactic
 
-(*s Introduction tactics with eliminations. *)
+(** {6 Introduction tactics with eliminations. } *)
 
 val intro_pattern  : identifier move_location -> intro_pattern_expr -> tactic
 val intro_patterns : intro_pattern_expr located list -> tactic
 val intros_pattern :
   identifier move_location -> intro_pattern_expr located list -> tactic
 
-(*s Exact tactics. *)
+(** {6 Exact tactics. } *)
 
 val assumption       : tactic
 val exact_no_check   : constr -> tactic
@@ -119,7 +117,7 @@ val vm_cast_no_check : constr -> tactic
 val exact_check      : constr -> tactic
 val exact_proof      : Topconstr.constr_expr -> tactic
 
-(*s Reduction tactics. *)
+(** {6 Reduction tactics. } *)
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
@@ -156,7 +154,7 @@ val pattern_option    :
 val reduce            : red_expr -> clause -> tactic
 val unfold_constr     : global_reference -> tactic
 
-(*s Modification of the local context. *)
+(** {6 Modification of the local context. } *)
 
 val clear         : identifier list -> tactic
 val clear_body    : identifier list -> tactic
@@ -169,7 +167,7 @@ val rename_hyp    : (identifier * identifier) list -> tactic
 
 val revert        : identifier list -> tactic
 
-(*s Resolution tactics. *)
+(** {6 Resolution tactics. } *)
 
 val apply_type : constr -> constr list -> tactic
 val apply_term : constr -> constr list -> tactic
@@ -193,7 +191,7 @@ val apply_in :
 
 val simple_apply_in : identifier -> constr -> tactic
 
-(*s Elimination tactics. *)
+(** {6 Elimination tactics. } *)
 
 
 (*
@@ -219,36 +217,36 @@ val simple_apply_in : identifier -> constr -> tactic
   Principles taken from functional induction have the final (f...).
 *)
 
-(* [rel_contexts] and [rel_declaration] actually contain triples, and
+(** [rel_contexts] and [rel_declaration] actually contain triples, and
    lists are actually in reverse order to fit [compose_prod]. *)
 type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
-  index: int;              (* index of the elimination type in the scheme *)
-  params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
-  nparams: int;            (* number of parameters *)
-  predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
-  npredicates: int;        (* Number of predicates *)
-  branches: rel_context;   (* branchr,...,branch1 *)
-  nbranches: int;          (* Number of branches *)
-  args: rel_context;       (* (xni, Ti_ni) ... (x1, Ti_1) *)
-  nargs: int;              (* number of arguments *)
-  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
+  index: int;              (** index of the elimination type in the scheme *)
+  params: rel_context;     (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  nparams: int;            (** number of parameters *)
+  predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  npredicates: int;        (** Number of predicates *)
+  branches: rel_context;   (** branchr,...,branch1 *)
+  nbranches: int;          (** Number of branches *)
+  args: rel_context;       (** (xni, Ti_ni) ... (x1, Ti_1) *)
+  nargs: int;              (** number of arguments *)
+  indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni)
 				     if HI is in premisses, None otherwise *)
-  concl: types;            (* Qi x1...xni HI (f...), HI and (f...)
+  concl: types;            (** Qi x1...xni HI (f...), HI and (f...)
 			      are optional and mutually exclusive *)
-  indarg_in_concl: bool;   (* true if HI appears at the end of conclusion *)
-  farg_in_concl: bool;     (* true if (f...) appears at the end of conclusion *)
+  indarg_in_concl: bool;   (** true if HI appears at the end of conclusion *)
+  farg_in_concl: bool;     (** true if (f...) appears at the end of conclusion *)
 }
 
 
 val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme
 val rebuild_elimtype_from_scheme: elim_scheme -> types
 
-(* elim principle with the index of its inductive arg *)
+(** elim principle with the index of its inductive arg *)
 type eliminator = {
-  elimindex : int option;  (* None = find it automatically *)
+  elimindex : int option;  (** None = find it automatically *)
   elimbody : constr with_bindings
 }
 
@@ -278,7 +276,7 @@ val new_induct : evars_flag -> constr with_bindings induction_arg list ->
     intro_pattern_expr located option * intro_pattern_expr located option ->
       clause option -> tactic
 
-(*s Case analysis tactics. *)
+(** {6 Case analysis tactics. } *)
 
 val general_case_analysis : evars_flag -> constr with_bindings ->  tactic
 val simplest_case         : constr -> tactic
@@ -289,7 +287,7 @@ val new_destruct : evars_flag -> constr with_bindings induction_arg list ->
     intro_pattern_expr located option * intro_pattern_expr located option ->
       clause option -> tactic
 
-(*s Generic case analysis / induction tactics. *)
+(** {6 Generic case analysis / induction tactics. } *)
 
 val induction_destruct : rec_flag -> evars_flag ->
   (constr with_bindings induction_arg list *
@@ -298,12 +296,12 @@ val induction_destruct : rec_flag -> evars_flag ->
   list *
   clause option -> tactic
 
-(*s Eliminations giving the type instead of the proof. *)
+(** {6 Eliminations giving the type instead of the proof. } *)
 
 val case_type         : constr  -> tactic
 val elim_type         : constr  -> tactic
 
-(*s Some eliminations which are frequently used. *)
+(** {6 Some eliminations which are frequently used. } *)
 
 val impE : identifier -> tactic
 val andE : identifier -> tactic
@@ -313,7 +311,7 @@ val dAnd : clause -> tactic
 val dorE : bool -> clause ->tactic
 
 
-(*s Introduction tactics. *)
+(** {6 Introduction tactics. } *)
 
 val constructor_tac      : evars_flag -> int option -> int ->
   constr bindings -> tactic
@@ -332,7 +330,7 @@ val simplest_left        : tactic
 val simplest_right       : tactic
 val simplest_split       : tactic
 
-(*s Logical connective tactics. *)
+(** {6 Logical connective tactics. } *)
 
 val register_setoid_reflexivity : tactic -> unit
 val reflexivity_red             : bool -> tactic
@@ -368,7 +366,7 @@ val pose_proof : name -> constr -> tactic
 
 val generalize      : constr list -> tactic
 val generalize_gen  : ((occurrences * constr) * name) list -> tactic
-val generalize_dep  : ?with_let:bool (* Don't lose let bindings *) -> constr  -> tactic
+val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -> tactic
 
 val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
 val resolve_classes : tactic
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index aea49b073..973cc0e5b 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -1,25 +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*)
 
-(*i*)
 open Term
 open Pattern
 open Libnames
 open Names
-(*i*)
 
-(* Discrimination nets of terms. *)
+(** Discrimination nets of terms. *)
 
-(* This module registers actions (typically tactics) mapped to patterns *)
+(** This module registers actions (typically tactics) mapped to patterns *)
 
-(* Patterns are stocked linearly as the list of its node in prefix
+(** Patterns are stocked linearly as the list of its node in prefix
 order in such a way patterns having the same prefix have this common
 prefix shared and the seek for the action associated to the patterns
 that a term matches are found in time proportional to the maximal
@@ -38,21 +36,21 @@ sig
     
   val create : unit -> t
     
-  (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *)
+  (** [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *)
     
   val add : t -> transparent_state -> (constr_pattern * Z.t) -> t
     
   val rmv : t -> transparent_state -> (constr_pattern * Z.t) -> t
     
-  (* [lookup t c] looks for patterns (with their action) matching term [c] *)
+  (** [lookup t c] looks for patterns (with their action) matching term [c] *)
     
   val lookup : t -> transparent_state -> constr -> (constr_pattern * Z.t) list
     
   val app : ((constr_pattern * Z.t) -> unit) -> t -> unit
 
     
-  (*i*)
-  (* These are for Nbtermdn *)
+  (**/**)
+  (** These are for Nbtermdn *)
  
   type term_label = 
     | GRLabel of global_reference
@@ -68,5 +66,5 @@ sig
   val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option
   val constr_val_discr : constr -> (term_label * constr list) lookup_res
     
-(*i*)
+(**/**)
 end