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

10 files changed, 218 insertions, 234 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 2533fc537..a97b85ed9 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.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
@@ -19,35 +18,32 @@ open Evarutil
 open Mod_subst
 open Rawterm
 open Unification
-(*i*)
 
-(***************************************************************)
-(* The Type of Constructions clausale environments. *)
+(** {6 The Type of Constructions clausale environments.} *)
 
-(* [env] is the typing context
- * [evd] is the mapping from metavar and evar numbers to their types
- *       and values.
- * [templval] is the template which we are trying to fill out.
- * [templtyp] is its type.
- *)
 type clausenv = {
-  env      : env;
-  evd      : evar_map;
-  templval : constr freelisted;
-  templtyp : constr freelisted }
-
-(* Substitution is not applied on templenv (because [subst_clenv] is
+  env      : env; (** the typing context *)
+  evd      : evar_map; (** the mapping from metavar and evar numbers to their 
+			   types and values *)
+  templval : constr freelisted; (** the template which we are trying to fill 
+				    out *)
+  templtyp : constr freelisted (** its type *)}
+
+(** Substitution is not applied on templenv (because [subst_clenv] is
    applied only on hints which typing env is overwritten by the
    goal env) *)
 val subst_clenv : substitution -> clausenv -> clausenv
 
-(* subject of clenv (instantiated) *)
+(** subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
-(* type of clenv (instantiated) *)
+
+(** type of clenv (instantiated) *)
 val clenv_type      : clausenv -> types
-(* substitute resolved metas *)
+
+(** substitute resolved metas *)
 val clenv_nf_meta   : clausenv -> constr -> constr
-(* type of a meta in clenv context *)
+
+(** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
 val mk_clenv_from : Goal.goal sigma -> constr * types -> clausenv
@@ -56,25 +52,23 @@ val mk_clenv_from_n :
 val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
 
-(***************************************************************)
-(* linking of clenvs *)
+(** {6 linking of clenvs } *)
 
 val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
 val clenv_fchain :
   ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
-(***************************************************************)
-(* Unification with clenvs *)
+(** {6 Unification with clenvs } *)
 
-(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
+(** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
 val clenv_unify :
   bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
-(* unifies the concl of the goal with the type of the clenv *)
+(** unifies the concl of the goal with the type of the clenv *)
 val clenv_unique_resolver :
   bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
-(* same as above ([allow_K=false]) but replaces remaining metas
+(** same as above ([allow_K=false]) but replaces remaining metas
    with fresh evars if [evars_flag] is [true] *)
 val evar_clenv_unique_resolver :
   bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
@@ -83,12 +77,11 @@ val clenv_dependent : bool -> clausenv -> metavariable list
 
 val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
 
-(***************************************************************)
-(* Bindings *)
+(** {6 Bindings } *)
 
 type arg_bindings = constr explicit_bindings
 
-(* bindings where the key is the position in the template of the
+(** bindings where the key is the position in the template of the
    clenv (dependent or not). Positions can be negative meaning to
    start from the rightmost argument of the template. *)
 val clenv_independent : clausenv -> metavariable list
@@ -96,23 +89,23 @@ val clenv_missing : clausenv -> metavariable list
 
 val clenv_constrain_last_binding : constr -> clausenv -> clausenv
 
-(* defines metas corresponding to the name of the bindings *)
+(** defines metas corresponding to the name of the bindings *)
 val clenv_match_args : arg_bindings -> clausenv -> clausenv
 
 val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
-(* start with a clenv to refine with a given term with bindings *)
+(** start with a clenv to refine with a given term with bindings *)
 
-(* the arity of the lemma is fixed *)
-(* the optional int tells how many prods of the lemma have to be used *)
-(* use all of them if None *)
+(** the arity of the lemma is fixed 
+   the optional int tells how many prods of the lemma have to be used 
+   use all of them if None *)
 val make_clenv_binding_apply :
   Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
    clausenv
 val make_clenv_binding :
   Goal.goal sigma -> constr * constr -> constr bindings -> clausenv
 
-(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
+(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
    [lmetas] is a list of metas to be applied to a proof of [t] so that
    it produces the unification pattern [ccl]; [sigma'] is [sigma]
    extended with [lmetas]; if [n] is defined, it limits the size of
@@ -124,20 +117,19 @@ val make_clenv_binding :
 val clenv_environments :
  evar_map -> int option -> types -> evar_map * constr list * types
 
-(* [clenv_environments_evars env sigma n t] does the same but returns
+(** [clenv_environments_evars env sigma n t] does the same but returns
    a list of Evar's defined in [env] and extends [sigma] accordingly *)
 val clenv_environments_evars :
  env -> evar_map -> int option -> types -> evar_map * constr list * types
 
-(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
+(** [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
 val clenv_conv_leq :
  env -> evar_map -> types -> constr -> int -> constr list
 
-(* if the clause is a product, add an extra meta for this product *)
+(** if the clause is a product, add an extra meta for this product *)
 exception NotExtensibleClause
 val clenv_push_prod : clausenv -> clausenv
 
-(***************************************************************)
-(* Pretty-print *)
+(** {6 Pretty-print } *)
 val pr_clenv : clausenv -> Pp.std_ppcmds
 
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 96fb262a1..02bf86641 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Util
 open Names
 open Term
@@ -18,9 +17,8 @@ open Clenv
 open Proof_type
 open Tacexpr
 open Unification
-(*i*)
 
-(* Tactics *)
+(** Tactics *)
 val unify : ?flags:unify_flags -> constr -> tactic
 val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> tactic
 val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic
@@ -29,5 +27,5 @@ val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
 val clenv_value_cast_meta : clausenv -> constr
 
-(* Compatibility, use res_pf ?with_evars:true instead *)
+(** Compatibility, use res_pf ?with_evars:true instead *)
 val e_res_pf : clausenv -> tactic
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 28c79d11e..ff986f3e6 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Names
 open Term
 open Environ
@@ -16,9 +15,8 @@ open Evd
 open Refiner
 open Pretyping
 open Rawterm
-(*i*)
 
-(* Refinement of existential variables. *)
+(** Refinement of existential variables. *)
 
 val w_refine : evar * evar_info ->
   (var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map
@@ -26,4 +24,4 @@ val w_refine : evar * evar_info ->
 val instantiate_pf_com :
   Evd.evar -> Topconstr.constr_expr -> Evd.evar_map -> Evd.evar_map
 
-(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
+(** the instantiate tactic was moved to [tactics/evar_tactics.ml] *)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 560e57736..eec3de730 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -1,28 +1,26 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Names
 open Term
 open Sign
 open Evd
 open Environ
 open Proof_type
-(*i*)
 
-(* This suppresses check done in [prim_refiner] for the tactic given in
+(** This suppresses check done in [prim_refiner] for the tactic given in
    argument; works by side-effect *)
 
 val with_check    : tactic -> tactic
 
-(* [without_check] respectively means:\\
+(** [without_check] respectively means:\\
   [Intro]: no check that the name does not exist\\
   [Intro_after]: no check that the name does not exist and that variables in
      its type does not escape their scope\\
@@ -32,7 +30,7 @@ val with_check    : tactic -> tactic
   no check that the name exist and that its type is convertible\\
 *)
 
-(* The primitive refiner. *)
+(** The primitive refiner. *)
 
 val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
 
@@ -41,7 +39,7 @@ type proof_variable
 
 val proof_variable_index : identifier -> proof_variable list -> int
 
-(*s Refiner errors. *)
+(** {6 Refiner errors. } *)
 
 type refiner_error =
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9e24061d3..47b741f5d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.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 Pp
 open Names
@@ -18,60 +17,62 @@ open Environ
 open Decl_kinds
 open Tacmach
 open Tacexpr
-(*i*)
 
-
-(*s Several proofs can be opened simultaneously but at most one is
+(** Several proofs can be opened simultaneously but at most one is
    focused at some time. The following functions work by side-effect
    on current set of open proofs. In this module, ``proofs'' means an
    open proof (something started by vernacular command [Goal], [Lemma]
    or [Theorem]), and ``goal'' means a subgoal of the current focused
    proof *)
 
-(*s [refining ()] tells if there is some proof in progress, even if a not
+(** {6 Sect } *)
+(** [refining ()] tells if there is some proof in progress, even if a not
    focused one *)
 
 val refining : unit -> bool
 
-(* [check_no_pending_proofs ()] fails if there is still some proof in
+(** [check_no_pending_proofs ()] fails if there is still some proof in
    progress *)
 
 val check_no_pending_proofs : unit -> unit
 
-(*s [delete_proof name] deletes proof of name [name] or fails if no proof
+(** {6 Sect } *)
+(** [delete_proof name] deletes proof of name [name] or fails if no proof
     has this name *)
 
 val delete_proof : identifier located -> unit
 
-(* [delete_current_proof ()] deletes current focused proof or fails if
+(** [delete_current_proof ()] deletes current focused proof or fails if
     no proof is focused *)
 
 val delete_current_proof : unit -> unit
 
-(* [delete_all_proofs ()] deletes all open proofs if any *)
+(** [delete_all_proofs ()] deletes all open proofs if any *)
 
 val delete_all_proofs : unit -> unit
 
-(*s [undo n] undoes the effect of the last [n] tactics applied to the
+(** {6 Sect } *)
+(** [undo n] undoes the effect of the last [n] tactics applied to the
     current proof; it fails if no proof is focused or if the ``undo''
     stack is exhausted *)
 
 val undo : int -> unit
 
-(* [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
+(** [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
    is the depth of the undo stack). *)
 val undo_todepth : int -> unit 
 
-(* Returns the depth of the current focused proof stack, this is used
+(** Returns the depth of the current focused proof stack, this is used
    to put informations in coq prompt (in emacs mode). *)
 val current_proof_depth: unit -> int
 
-(* [set_undo (Some n)] used to set the size of the ``undo'' stack. 
+(** [set_undo (Some n)] used to set the size of the ``undo'' stack. 
     These function now do nothing and will disapear. *)
 val set_undo : int option -> unit
 val get_undo : unit -> int option
 
-(*s [start_proof s str env t hook tac] starts a proof of name [s] and
+(** {6 Sect } *)
+(** [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
     proof end (e.g. to declare the built constructions as a coercion
     or a setoid morphism); init_tac is possibly a tactic to
@@ -85,27 +86,29 @@ val start_proof :
   ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
   declaration_hook -> unit
 
-(* [restart_proof ()] restarts the current focused proof from the beginning
+(** [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
 
 val restart_proof : unit -> unit
 
-(*s [resume_last_proof ()] focus on the last unfocused proof or fails
+(** {6 Sect } *)
+(** [resume_last_proof ()] focus on the last unfocused proof or fails
    if there is no suspended proofs *)
 
 val resume_last_proof : unit -> unit
 
-(* [resume_proof name] focuses on the proof of name [name] or
+(** [resume_proof name] focuses on the proof of name [name] or
    raises [UserError] if no proof has name [name] *)
 
 val resume_proof : identifier located -> unit
 
-(* [suspend_proof ()] unfocuses the current focused proof or
+(** [suspend_proof ()] unfocuses the current focused proof or
    failed with [UserError] if no proof is currently focused *)
 
 val suspend_proof : unit -> unit
 
-(*s [cook_proof opacity] turns the current proof (assumed completed) into
+(** {6 Sect } *)
+(** [cook_proof opacity] turns the current proof (assumed completed) into
     a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed;
     it also tells if the guardness condition has to be inferred. *)
@@ -115,63 +118,67 @@ val cook_proof : (Proof.proof -> unit) ->
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
      declaration_hook)
 
-(* To export completed proofs to xml *)
+(** To export completed proofs to xml *)
 val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
 
-(*s [get_Proof.proof ()] returns the current focused pending proof or
+(** {6 Sect } *)
+(** [get_Proof.proof ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
 
 val get_pftreestate : unit -> Proof.proof
 
-(* [get_goal_context n] returns the context of the [n]th subgoal of
+(** [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
 
 val get_goal_context : int -> Evd.evar_map * env
 
-(* [get_current_goal_context ()] works as [get_goal_context 1] *)
+(** [get_current_goal_context ()] works as [get_goal_context 1] *)
 
 val get_current_goal_context : unit -> Evd.evar_map * env
 
-(* [current_proof_statement] *)
+(** [current_proof_statement] *)
 
 val current_proof_statement :
   unit -> identifier * goal_kind * types * declaration_hook
 
-(*s [get_current_proof_name ()] return the name of the current focused
+(** {6 Sect } *)
+(** [get_current_proof_name ()] return the name of the current focused
     proof or failed if no proof is focused *)
 
 val get_current_proof_name : unit -> identifier
 
-(* [get_all_proof_names ()] returns the list of all pending proof names *)
+(** [get_all_proof_names ()] returns the list of all pending proof names *)
 
 val get_all_proof_names : unit -> identifier list
 
-(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate
+(** {6 Sect } *)
+(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
     by [solve_nth] *)
 
 val set_end_tac : tactic -> unit
 
-(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
+(** {6 Sect } *)
+(** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
    current focused proof or raises a UserError if no proof is focused or
    if there is no [n]th subgoal *)
 
 val solve_nth : ?with_end_tac:bool -> int -> tactic -> unit
 
-(* [by tac] applies tactic [tac] to the 1st subgoal of the current
+(** [by tac] applies tactic [tac] to the 1st subgoal of the current
    focused proof or raises a UserError if there is no focused proof or
    if there is no more subgoals *)
 
 val by : tactic -> unit
 
-(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined
+(** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
    existential variable of the current focused proof by [c] or raises a
    UserError if no proof is focused or if there is no such [n]th
    existential variable *)
 
 val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
 
-(* [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
+(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
 
 val build_constant_by_tactic : named_context_val -> types -> tactic ->
   Entries.definition_entry
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9692f19bc..7d8875302 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.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 Environ
 open Evd
 open Names
@@ -20,9 +19,8 @@ open Rawterm
 open Genarg
 open Nametab
 open Pattern
-(*i*)
 
-(* This module defines the structure of proof tree and the tactic type. So, it
+(** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
 
 type goal = Goal.goal
@@ -44,35 +42,33 @@ type prim_rule =
   | Rename of identifier * identifier
   | Change_evars
 
-(* The type [goal sigma] is the type of subgoal. It has the following form
-\begin{verbatim}
-   it    = { evar_concl = [the conclusion of the subgoal]
+(** The type [goal sigma] is the type of subgoal. It has the following form
+{v   it    = \{ evar_concl = [the conclusion of the subgoal]
              evar_hyps = [the hypotheses of the subgoal]
              evar_body = Evar_Empty;
-             evar_info = { pgm    : [The Realizer pgm if any]
-                           lc     : [Set of evar num occurring in subgoal] }}
-   sigma = { stamp = [an int chardacterizing the ed field, for quick compare]
+             evar_info = \{ pgm    : [The Realizer pgm if any]
+                           lc     : [Set of evar num occurring in subgoal] \}\}
+   sigma = \{ stamp = [an int chardacterizing the ed field, for quick compare]
              ed : [A set of existential variables depending in the subgoal]
                number of first evar,
-               it = { evar_concl = [the type of first evar]
+               it = \{ evar_concl = [the type of first evar]
                       evar_hyps = [the context of the evar]
                       evar_body = [the body of the Evar if any]
-                      evar_info = { pgm    : [Useless ??]
+                      evar_info = \{ pgm    : [Useless ??]
                                     lc     : [Set of evars occurring
-                                              in the type of evar] } };
+                                              in the type of evar] \} \};
                ...
                number of last evar,
-               it = { evar_concl = [the type of evar]
+               it = \{ evar_concl = [the type of evar]
                       evar_hyps = [the context of the evar]
                       evar_body = [the body of the Evar if any]
-                      evar_info = { pgm    : [Useless ??]
+                      evar_info = \{ pgm    : [Useless ??]
                                     lc     : [Set of evars occurring
-                                              in the type of evar] } } }
-   }
-\end{verbatim}
+                                              in the type of evar] \} \} \} v}
 *)
 
-(*s Proof trees.
+(** {6 Sect } *)
+(** Proof trees.
   [ref] = [None] if the goal has still to be proved,
   and [Some (r,l)] if the rule [r] was applied to the goal
   and gave [l] as subproofs to be completed.
@@ -90,7 +86,7 @@ and rule =
   | Daimon
 
 and compound_rule=
-  (* the boolean of Tactic tells if the default tactic is used *)
+  (** the boolean of Tactic tells if the default tactic is used *)
   | Tactic of tactic_expr * bool
 
 and tactic_expr =
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 03d97ce35..199130b5f 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.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*)
 
@@ -22,23 +22,24 @@ type red_expr =
 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
 val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
-(* [true] if we should use the vm to verify the reduction *)
 
-(* Adding a custom reduction (function to be use at the ML level)
+(** [true] if we should use the vm to verify the reduction *)
+
+(** Adding a custom reduction (function to be use at the ML level)
    NB: the effect is permanent. *)
 val declare_reduction : string -> reduction_function -> unit
 
-(* Adding a custom reduction (function to be called a vernac command).
+(** Adding a custom reduction (function to be called a vernac command).
    The boolean flag is the locality. *)
 val declare_red_expr : bool -> string -> red_expr -> unit
 
-(* Opaque and Transparent commands. *)
+(** Opaque and Transparent commands. *)
 
-(* Sets the expansion strategy of a constant. When the boolean is
+(** Sets the expansion strategy of a constant. When the boolean is
    true, the effect is non-synchronous (i.e. it does not survive
    section and module closure). *)
 val set_strategy :
   bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit
 
-(* call by value normalisation function using the virtual machine *)
+(** call by value normalisation function using the virtual machine *)
 val cbv_vm : reduction_function
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 77f2e48a7..958560044 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.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 Term
 open Sign
 open Evd
 open Proof_type
 open Tacexpr
 open Logic
-(*i*)
 
-(* The refiner (handles primitive rules and high-level tactics). *)
+(** The refiner (handles primitive rules and high-level tactics). *)
 
 val sig_it  : 'a sigma -> 'a
 val project : 'a sigma -> evar_map
@@ -30,9 +28,9 @@ val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :
   evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
 
-(*s Hiding the implementation of tactics. *)
+(** {6 Hiding the implementation of tactics. } *)
 
-(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
+(** [abstract_tactic tac] hides the (partial) proof produced by [tac] under
    a single proof node. The boolean tells if the default tactic is used. *)
 (* spiwack: currently here for compatibility, abstract_operation 
     is a second projection *)
@@ -44,83 +42,83 @@ val abstract_extended_tactic :
 
 val refiner : rule -> tactic
 
-(*s Tacticals. *)
+(** {6 Tacticals. } *)
 
-(* [tclNORMEVAR] forces propagation of evar constraints *)
+(** [tclNORMEVAR] forces propagation of evar constraints *)
 val tclNORMEVAR       : tactic
 
-(* [tclIDTAC] is the identity tactic without message printing*)
+(** [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
 val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
 
-(* [tclEVARS sigma] changes the current evar map *)
+(** [tclEVARS sigma] changes the current evar map *)
 val tclEVARS : evar_map -> tactic
 
-(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
 val tclTHEN          : tactic -> tactic -> tactic
 
-(* [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
+(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
    convenient than [tclTHEN] when [n] is large *)
 val tclTHENLIST      : tactic list -> tactic
 
-(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 
-(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
-   [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *)
+(** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
+   [(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *)
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 
-(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+(** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
    to the last resulting subgoal (previously called [tclTHENL]) *)
 val tclTHENLAST         : tactic -> tactic -> tactic
 
-(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
    to the first resulting subgoal *)
 val tclTHENFIRST         : tactic -> tactic -> tactic
 
-(* [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
+(** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
    [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
    an error if the number of resulting subgoals is not [n] *)
 val tclTHENSV         : tactic -> tactic array -> tactic
 
-(* Same with a list of tactics *)
+(** Same with a list of tactics *)
 val tclTHENS         : tactic -> tactic list -> tactic
 
-(* [tclTHENST] is renamed [tclTHENSFIRSTn]
+(** [tclTHENST] is renamed [tclTHENSFIRSTn]
 val tclTHENST        : tactic -> tactic array -> tactic -> tactic
 *)
 
-(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
+(** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
    subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
    error if the number of resulting subgoals is strictly less than [n+m] *)
 val tclTHENS3PARTS     : tactic -> tactic array -> tactic -> tactic array -> tactic
 
-(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
+(** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
    last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
 val tclTHENSLASTn     : tactic -> tactic -> tactic array -> tactic
 
-(* [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
+(** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
    applies [t1],...,[tn] on the first [n] resulting subgoals and
    [tac2] for the remaining last subgoals (previously called tclTHENST) *)
 val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
 
-(* [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
+(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
    applies [t1],...,[tn] on the last [n] resulting subgoals and leaves
    unchanged the other subgoals *)
 val tclTHENLASTn    : tactic -> tactic array -> tactic
 
-(* [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
+(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
    applies [t1],...,[tn] on the first [n] resulting subgoals and leaves
    unchanged the other subgoals (previously called [tclTHENSI]) *)
 val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 
-(* A special exception for levels for the Fail tactic *)
+(** A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.std_ppcmds Lazy.t
 
-(* Takes an exception and either raise it at the next
+(** Takes an exception and either raise it at the next
    level or do nothing. *)
 val catch_failerror  : exn -> unit
 
@@ -142,20 +140,20 @@ val tclPROGRESS      : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
 val tclINFO          : tactic -> tactic
 
-(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
+(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
    if it succeeds, applies [tac2] to the resulting subgoals,
    and if not applies [tac3] to the initial goal [gls] *)
 val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
 val tclIFTHENSELSE   : tactic -> tactic list -> tactic ->tactic
 val tclIFTHENSVELSE   : tactic -> tactic array -> tactic ->tactic
 
-(* [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
+(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1]
    has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed.
    Equivalent to [(tac1;try tac2)||tac2] *)
 
 val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
-(*s Tactics handling a list of goals. *)
+(** {6 Tactics handling a list of goals. } *)
 
 type tactic_list = goal list sigma -> goal list sigma
 
@@ -167,10 +165,8 @@ val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
 val tactic_list_tactic : tactic_list -> tactic
 val goal_goal_list     : 'a sigma -> 'a list sigma
 
-(* [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which
+(** [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which
    may have unresolved holes; if [solve_holes] these holes must be
    resolved after application of the tactic; [sigma] must be an
    extension of the sigma of the goal *)
 val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic
-
-(*s Pretty-printers. *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f4bb1d922..cf704d101 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Names
 open Term
 open Sign
@@ -21,9 +20,8 @@ open Redexpr
 open Tacexpr
 open Rawterm
 open Pattern
-(*i*)
 
-(* Operations for handling terms under a local typing context. *)
+(** Operations for handling terms under a local typing context. *)
 
 type 'a sigma   = 'a Evd.sigma;;
 type tactic     = Proof_type.tactic;;
@@ -89,7 +87,7 @@ val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
 val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
 
-(*s The most primitive tactics. *)
+(** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
 val introduction_no_check     : identifier -> tactic
@@ -108,7 +106,7 @@ val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> int -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> int -> tactic
 
-(*s The most primitive tactics with consistency and type checking *)
+(** {6 The most primitive tactics with consistency and type checking } *)
 
 val introduction     : identifier -> tactic
 val internal_cut     : bool -> identifier -> types -> tactic
@@ -121,7 +119,7 @@ val thin_body        : identifier list -> tactic
 val move_hyp         : bool -> identifier -> identifier move_location -> tactic
 val rename_hyp       : (identifier*identifier) list -> tactic
 
-(*s Tactics handling a list of goals. *)
+(** {6 Tactics handling a list of goals. } *)
 
 type validation_list = proof_tree list -> proof_tree list
 
@@ -135,6 +133,6 @@ val tactic_list_tactic : tactic_list -> tactic
 val tclFIRSTLIST       : tactic_list list -> tactic_list
 val tclIDTAC_list      : tactic_list
 
-(*s Pretty-printing functions (debug only). *)
+(** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
 val pr_glls   : goal list sigma -> Pp.std_ppcmds
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 0a5e6087b..f27540315 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
@@ -16,7 +16,7 @@ open Names
 open Tacexpr
 open Term
 
-(* This module intends to be a beginning of debugger for tactic expressions.
+(** This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
    complete panel of commands dedicated to a proof assistant framework *)
 
@@ -27,50 +27,50 @@ val set_match_rule_printer :
   ((Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
     unit
 
-(* Debug information *)
+(** Debug information *)
 type debug_info =
   | DebugOn of int
   | DebugOff
 
-(* Prints the state and waits *)
+(** Prints the state and waits *)
 val debug_prompt :
   int -> goal sigma -> glob_tactic_expr -> (debug_info -> 'a) -> 'a
 
-(* Prints a constr *)
+(** Prints a constr *)
 val db_constr : debug_info -> env -> constr -> unit
 
-(* Prints the pattern rule *)
+(** Prints the pattern rule *)
 val db_pattern_rule :
   debug_info -> int -> (Genarg.rawconstr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit
 
-(* Prints a matched hypothesis *)
+(** Prints a matched hypothesis *)
 val db_matched_hyp :
   debug_info -> env -> identifier * constr option * constr -> name -> unit
 
-(* Prints the matched conclusion *)
+(** Prints the matched conclusion *)
 val db_matched_concl : debug_info -> env -> constr -> unit
 
-(* Prints a success message when the goal has been matched *)
+(** Prints a success message when the goal has been matched *)
 val db_mc_pattern_success : debug_info -> unit
 
-(* Prints a failure message for an hypothesis pattern *)
+(** Prints a failure message for an hypothesis pattern *)
 val db_hyp_pattern_failure :
   debug_info -> env -> name * constr_pattern match_pattern -> unit
 
-(* Prints a matching failure message for a rule *)
+(** Prints a matching failure message for a rule *)
 val db_matching_failure : debug_info -> unit
 
-(* Prints an evaluation failure message for a rule *)
+(** Prints an evaluation failure message for a rule *)
 val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit
 
-(* An exception handler *)
+(** An exception handler *)
 val explain_logic_error: (exn -> Pp.std_ppcmds) ref
 
-(* For use in the Ltac debugger: some exception that are usually
+(** For use in the Ltac debugger: some exception that are usually
    consider anomalies are acceptable because they are caught later in
    the process that is being debugged.  One should not require
    from users that they report these anomalies. *)
 val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
 
-(* Prints a logic failure message for a rule *)
+(** Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit