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

13 files changed, 265 insertions, 272 deletions

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 08a74e614..f52ec8fd8 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Util
 open Names
 open Term
@@ -21,12 +20,11 @@ open Rawterm
 open Pattern
 open Topconstr
 open Notation
-(*i*)
 
-(* v7->v8 translation *)
+(** v7->v8 translation *)
 val check_same_type : constr_expr -> constr_expr -> unit
 
-(* Translation of pattern, cases pattern, rawterm and term into syntax
+(** Translation of pattern, cases pattern, rawterm and term into syntax
    trees for printing *)
 
 val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
@@ -34,7 +32,7 @@ val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
 val extern_rawtype : Idset.t -> rawconstr -> constr_expr
 val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
 
-(* If [b=true] in [extern_constr b env c] then the variables in the first
+(** If [b=true] in [extern_constr b env c] then the variables in the first
    level of quantification clashing with the variables in [env] are renamed *)
 
 val extern_constr : bool -> env -> constr -> constr_expr
@@ -45,7 +43,7 @@ val extern_sort : sorts -> rawsort
 val extern_rel_context : constr option -> env ->
   rel_context -> local_binder list
 
-(* Printing options *)
+(** Printing options *)
 val print_implicits : bool ref
 val print_implicits_defensive : bool ref
 val print_arguments : bool ref
@@ -55,25 +53,25 @@ val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
 
-(* Debug printing options *)
+(** Debug printing options *)
 val set_debug_global_reference_printer :
   (loc -> global_reference -> reference) -> unit
 
-(* This governs printing of implicit arguments. If [with_implicits] is
+(** This governs printing of implicit arguments. If [with_implicits] is
    on and not [with_arguments] then implicit args are printed prefixed
    by "!"; if [with_implicits] and [with_arguments] are both on the
    function and not the arguments is prefixed by "!" *)
 val with_implicits : ('a -> 'b) -> 'a -> 'b
 val with_arguments : ('a -> 'b) -> 'a -> 'b
 
-(* This forces printing of coercions *)
+(** This forces printing of coercions *)
 val with_coercions : ('a -> 'b) -> 'a -> 'b
 
-(* This forces printing universe names of Type{.} *)
+(** This forces printing universe names of Type\{.\} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
 
-(* This suppresses printing of numeral and symbols *)
+(** This suppresses printing of numeral and symbols *)
 val without_symbols : ('a -> 'b) -> 'a -> 'b
 
-(* This prints metas as anonymous holes *)
+(** This prints metas as anonymous holes *)
 val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 5a62541db..4ba2bc587 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.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
@@ -20,9 +19,9 @@ open Pattern
 open Topconstr
 open Termops
 open Pretyping
-(*i*)
 
-(*s Translation from front abstract syntax of term to untyped terms (rawconstr)
+(** {6 Sect } *)
+(** Translation from front abstract syntax of term to untyped terms (rawconstr)
 
    The translation performs:
 
@@ -33,7 +32,7 @@ open Pretyping
    - insert existential variables for implicit arguments
 *)
 
-(* To interpret implicits and arg scopes of recursive variables while
+(** To interpret implicits and arg scopes of recursive variables while
    internalizing inductive types and recursive definitions, and also
    projection while typing records.
 
@@ -49,11 +48,11 @@ type var_internalization_data =
     Impargs.implicits_list *
     scope_name option list
 
-(* A map of free variables to their implicit arguments and scopes *)
+(** A map of free variables to their implicit arguments and scopes *)
 type internalization_env =
     (identifier * var_internalization_data) list
 
-(* Contains also a list of identifiers to automatically apply to the variables*)
+(** Contains also a list of identifiers to automatically apply to the variables*)
 type full_internalization_env =
     identifier list * internalization_env
 
@@ -76,7 +75,7 @@ type ltac_sign = identifier list * unbound_ltac_var_map
 
 type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
 
-(*s Internalisation performs interpretation of global names and notations *)
+(** {6 Internalisation performs interpretation of global names and notations } *)
 
 val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 
@@ -92,15 +91,15 @@ val intern_pattern : env -> cases_pattern_expr ->
 
 val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
 
-(*s Composing internalization with pretyping *)
+(** {6 Composing internalization with pretyping } *)
 
-(* Main interpretation function *)
+(** Main interpretation function *)
 
 val interp_gen : typing_constraint -> evar_map -> env ->
   ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> constr
 
-(* Particular instances *)
+(** Particular instances *)
 
 val interp_constr : evar_map -> env ->
   constr_expr -> constr
@@ -115,7 +114,7 @@ val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * c
 val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env ->
   constr_expr -> types -> constr
 
-(* Accepting evars and giving back the manual implicits in addition. *)
+(** Accepting evars and giving back the manual implicits in addition. *)
 
 val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env ->
   ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits
@@ -134,29 +133,29 @@ val interp_casted_constr_evars : evar_map ref -> env ->
 val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env ->
   constr_expr -> types
 
-(*s Build a judgment  *)
+(** {6 Build a judgment  } *)
 
 val interp_constr_judgment : evar_map -> env -> constr_expr -> unsafe_judgment
 
-(* Interprets constr patterns *)
+(** Interprets constr patterns *)
 
 val intern_constr_pattern :
   evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> patvar list * constr_pattern
 
-(* Raise Not_found if syndef not bound to a name and error if unexisting ref *)
+(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
 val intern_reference : reference -> global_reference
 
-(* Expands abbreviations (syndef); raise an error if not existing *)
+(** Expands abbreviations (syndef); raise an error if not existing *)
 val interp_reference : ltac_sign -> reference -> rawconstr
 
-(* Interpret binders *)
+(** Interpret binders *)
 
 val interp_binder  : evar_map -> env -> name -> constr_expr -> types
 
 val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types
 
-(* Interpret contexts: returns extended env and context *)
+(** Interpret contexts: returns extended env and context *)
 
 val interp_context_gen : (env -> rawconstr -> types) ->
   (env -> rawconstr -> unsafe_judgment) ->
@@ -169,18 +168,18 @@ val interp_context : ?fail_anonymous:bool ->
 val interp_context_evars : ?fail_anonymous:bool ->
   evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
-(* Locating references of constructions, possibly via a syntactic definition *)
-(* (these functions do not modify the glob file) *)
+(** Locating references of constructions, possibly via a syntactic definition 
+   (these functions do not modify the glob file) *)
 
 val is_global : identifier -> bool
 val construct_reference : named_context -> identifier -> constr
 val global_reference : identifier -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
-(* Interprets into a abbreviatable constr *)
+(** Interprets into a abbreviatable constr *)
 
 val interp_aconstr : ?impls:full_internalization_env ->
   identifier list * identifier list -> constr_expr -> interpretation
 
-(* Globalization leak for Grammar *)
+(** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 6bb79c8b6..5148461a9 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -1,25 +1,25 @@
-(************************************************************************)
-(*  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 Libnames
 open Nametab
 open Term
 open Pattern
-(*i*)
 
-(*s This module collects the global references, constructions and
+(** {6 Sect } *)
+(** This module collects the global references, constructions and
     patterns of the standard library used in ocaml files *)
 
-(*s [find_reference caller_message [dir;subdir;...] s] returns a global
+(** {6 Sect } *)
+(** [find_reference caller_message [dir;subdir;...] s] returns a global
    reference to the name dir.subdir.(...).s; the corresponding module
    must have been required or in the process of being compiled so that
    it must be used lazyly; it raises an anomaly with the given message
@@ -29,39 +29,39 @@ type message = string
 
 val find_reference : message -> string list -> string -> global_reference
 
-(* [coq_reference caller_message [dir;subdir;...] s] returns a
+(** [coq_reference caller_message [dir;subdir;...] s] returns a
    global reference to the name Coq.dir.subdir.(...).s *)
 
 val coq_reference : message -> string list -> string -> global_reference
 
-(* idem but return a term *)
+(** idem but return a term *)
 
 val coq_constant : message -> string list -> string -> constr
 
-(* Synonyms of [coq_constant] and [coq_reference] *)
+(** Synonyms of [coq_constant] and [coq_reference] *)
 
 val gen_constant : message -> string list -> string -> constr
 val gen_reference :  message -> string list -> string -> global_reference
 
-(* Search in several modules (not prefixed by "Coq") *)
+(** Search in several modules (not prefixed by "Coq") *)
 val gen_constant_in_modules : string->string list list-> string -> constr
 val arith_modules : string list list
 val zarith_base_modules : string list list
 val init_modules : string list list
 
-(* For tactics/commands requiring vernacular libraries *)
+(** For tactics/commands requiring vernacular libraries *)
 val check_required_library : string list -> unit
 
-(*s Global references *)
+(** {6 Global references } *)
 
-(* Modules *)
+(** Modules *)
 val logic_module : dir_path
 val logic_type_module : dir_path
 
 val datatypes_module_name : string list
 val logic_module_name : string list
 
-(* Natural numbers *)
+(** Natural numbers *)
 val nat_path : full_path
 val glob_nat : global_reference
 val path_of_O : constructor
@@ -69,7 +69,7 @@ val path_of_S : constructor
 val glob_O : global_reference
 val glob_S : global_reference
 
-(* Booleans *)
+(** Booleans *)
 val glob_bool : global_reference
 val path_of_true : constructor
 val path_of_false : constructor
@@ -77,12 +77,13 @@ val glob_true : global_reference
 val glob_false : global_reference
 
 
-(* Equality *)
+(** Equality *)
 val glob_eq : global_reference
 val glob_identity : global_reference
 val glob_jmeq : global_reference
 
-(*s Constructions and patterns related to Coq initial state are unknown
+(** {6 Sect } *)
+(** Constructions and patterns related to Coq initial state are unknown
    at compile time. Therefore, we can only provide methods to build
    them at runtime. This is the purpose of the [constr delayed] and
    [constr_pattern delayed] types. Objects of this time needs to be
@@ -96,7 +97,7 @@ type coq_bool_data = {
   andb_true_intro : constr}
 val build_bool_type : coq_bool_data delayed
 
-(*s For Equality tactics *)
+(** {6 For Equality tactics } *)
 type coq_sigma_data = {
   proj1 : constr;
   proj2 : constr;
@@ -106,7 +107,8 @@ type coq_sigma_data = {
 
 val build_sigma_set : coq_sigma_data delayed
 val build_sigma_type : coq_sigma_data delayed
-(* Non-dependent pairs in Set from Datatypes *)
+
+(** Non-dependent pairs in Set from Datatypes *)
 val build_prod : coq_sigma_data delayed
 
 type coq_eq_data = {
@@ -121,17 +123,19 @@ val build_coq_eq_data : coq_eq_data delayed
 val build_coq_identity_data : coq_eq_data delayed
 val build_coq_jmeq_data : coq_eq_data delayed
 
-val build_coq_eq       : constr delayed (* = [(build_coq_eq_data()).eq] *)
-val build_coq_eq_refl  : constr delayed (* = [(build_coq_eq_data()).refl] *)
-val build_coq_eq_sym   : constr delayed (* = [(build_coq_eq_data()).sym] *)
+val build_coq_eq       : constr delayed (** = [(build_coq_eq_data()).eq] *)
+val build_coq_eq_refl  : constr delayed (** = [(build_coq_eq_data()).refl] *)
+val build_coq_eq_sym   : constr delayed (** = [(build_coq_eq_data()).sym] *)
 val build_coq_f_equal2 : constr delayed
 
-(* Data needed for discriminate and injection *)
+(** Data needed for discriminate and injection *)
 
 type coq_inversion_data = {
-  inv_eq   : constr; (* : forall params, t -> Prop *)
-  inv_ind  : constr; (* : forall params P y, eq params y -> P y *)
-  inv_congr: constr  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+  inv_eq   : constr; (** : forall params, args -> Prop *)
+  inv_ind  : constr; (** : forall params P (H : P params) args, eq params args 
+			 ->  P args *)
+  inv_congr: constr  (** : forall params B (f:t->B) args, eq params args -> 
+			 f params = f args *)
 }
 
 val build_coq_inversion_eq_data : coq_inversion_data delayed
@@ -139,21 +143,22 @@ val build_coq_inversion_identity_data : coq_inversion_data delayed
 val build_coq_inversion_jmeq_data : coq_inversion_data delayed
 val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 
-(* Specif *)
+(** Specif *)
 val build_coq_sumbool : constr delayed
 
-(*s Connectives *)
-(* The False proposition *)
+(** {6 Sect } *)
+(** Connectives 
+   The False proposition *)
 val build_coq_False : constr delayed
 
-(* The True proposition and its unique proof *)
+(** The True proposition and its unique proof *)
 val build_coq_True : constr delayed
 val build_coq_I : constr delayed
 
-(* Negation *)
+(** Negation *)
 val build_coq_not : constr delayed
 
-(* Conjunction *)
+(** Conjunction *)
 val build_coq_and : constr delayed
 val build_coq_conj : constr delayed
 val build_coq_iff : constr delayed
@@ -161,10 +166,10 @@ val build_coq_iff : constr delayed
 val build_coq_iff_left_proj : constr delayed
 val build_coq_iff_right_proj : constr delayed
 
-(* Disjunction *)
+(** Disjunction *)
 val build_coq_or : constr delayed
 
-(* Existential quantifier *)
+(** Existential quantifier *)
 val build_coq_ex : constr delayed
 
 val coq_eq_ref : global_reference lazy_t
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index f6d7baefe..7235fe172 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -1,12 +1,12 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id$ *)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
+
+(** {% $ %}Id: dumpglob.mli 11252 2008-07-24 11:16:48Z notin {% $ %} *)
 
 
 val open_glob_file : string -> unit
diff --git a/interp/genarg.mli b/interp/genarg.mli
index fab5ff33e..50abd351e 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
@@ -26,9 +26,9 @@ type 'a or_by_notation =
 
 val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc
 
-(* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
-(* in the environment by the effective calls to Intro, Inversion, etc *)
-(* The [constr_expr] field is [None] in TacDef though *)
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+   in the environment by the effective calls to Intro, Inversion, etc 
+   The [constr_expr] field is [None] in TacDef though *)
 type rawconstr_and_expr = rawconstr * constr_expr option
 
 type open_constr_expr = unit * constr_expr
@@ -51,9 +51,9 @@ and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
 val pr_intro_pattern : intro_pattern_expr located -> Pp.std_ppcmds
 val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
 
-(* The route of a generic argument, from parsing to evaluation
+(** The route of a generic argument, from parsing to evaluation
 
-\begin{verbatim}
+{% \begin{%}verbatim{% }%}
              parsing        in_raw                              out_raw
    char stream ----> rawtype ----> constr_expr generic_argument --------|
                           encapsulation                         decaps  |
@@ -76,7 +76,7 @@ val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
     |
     V
 effective use
-\end{verbatim}
+{% \end{%}verbatim{% }%}
 
 To distinguish between the uninterpreted (raw), globalized and
 interpreted worlds, we annotate the type [generic_argument] by a
@@ -84,7 +84,7 @@ phantom argument which is either [constr_expr], [rawconstr] or
 [constr].
 
 Transformation for each type :
-\begin{verbatim}
+{% \begin{%}verbatim{% }%}
 tag                            raw open type            cooked closed type
 
 BoolArgType                    bool                      bool
@@ -107,10 +107,10 @@ List0ArgType of argument_type
 List1ArgType of argument_type
 OptArgType of argument_type
 ExtraArgType of string         '_a                      '_b
-\end{verbatim}
+{% \end{%}verbatim{% }%}
 *)
 
-(* All of [rlevel], [glevel] and [tlevel] must be non convertible
+(** All of [rlevel], [glevel] and [tlevel] must be non convertible
    to ensure the injectivity of the type inference from type
    ['co generic_argument] to [('a,'co) abstract_argument_type];
    this guarantees that, for 'co fixed, the type of
@@ -222,7 +222,7 @@ val wit_pair :
   ('b,'co) abstract_argument_type ->
       ('a * 'b,'co) abstract_argument_type
 
-(* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
+(** ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
 type 'a generic_argument
 
 val fold_list0 :
@@ -238,7 +238,7 @@ val fold_pair :
  ('a generic_argument -> 'a generic_argument -> 'c) ->
       'a generic_argument -> 'c
 
-(* [app_list0] fails if applied to an argument not of tag [List0 t]
+(** [app_list0] fails if applied to an argument not of tag [List0 t]
     for some [t]; it's the responsability of the caller to ensure it *)
 
 val app_list0 : ('a generic_argument -> 'b generic_argument) ->
@@ -255,7 +255,7 @@ val app_pair :
       ('a generic_argument -> 'b generic_argument)
    -> 'a generic_argument -> 'b generic_argument
 
-(* create a new generic type of argument: force to associate
+(** create a new generic type of argument: force to associate
    unique ML types at each of the three levels *)
 val create_arg : string ->
       ('a,tlevel) abstract_argument_type
@@ -265,7 +265,7 @@ val create_arg : string ->
 val exists_argtype : string -> bool
 
 type argument_type =
-  (* Basic types *)
+  (** Basic types *)
   | BoolArgType
   | IntArgType
   | IntOrVarArgType
@@ -275,7 +275,7 @@ type argument_type =
   | IdentArgType of bool
   | VarArgType
   | RefArgType
-  (* Specific types *)
+  (** Specific types *)
   | SortArgType
   | ConstrArgType
   | ConstrMayEvalArgType
@@ -300,7 +300,7 @@ val out_gen :
   ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
 
 
-(* [in_generic] is used in combination with camlp4 [Gramext.action] magic
+(** [in_generic] is used in combination with camlp4 [Gramext.action] magic
 
    [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
 
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 1feae81f5..7362d7de5 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Names
 open Decl_kinds
 open Term
@@ -22,7 +21,6 @@ open Topconstr
 open Util
 open Libnames
 open Typeclasses
-(*i*)
 
 val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
 
@@ -30,7 +28,7 @@ val ids_of_list : identifier list -> Idset.t
 val destClassApp : constr_expr -> loc * reference * constr_expr list
 val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list
 
-(* Fragile, should be used only for construction a set of identifiers to avoid *)
+(** Fragile, should be used only for construction a set of identifiers to avoid *)
 
 val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
   identifier list -> identifier list
@@ -38,7 +36,7 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
 val free_vars_of_binders :
   ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
 
-(* Returns the generalizable free ids in left-to-right
+(** Returns the generalizable free ids in left-to-right
    order with the location of their first occurence *)
 
 val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t ->
diff --git a/interp/modintern.mli b/interp/modintern.mli
index e528b7af7..e025447b5 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.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 Declarations
 open Environ
 open Entries
@@ -16,16 +15,15 @@ open Util
 open Libnames
 open Names
 open Topconstr
-(*i*)
 
-(* Module expressions and module types are interpreted relatively to
+(** Module expressions and module types are interpreted relatively to
    eventual functor or funsig arguments. *)
 
 val interp_modtype : env -> module_ast -> module_struct_entry
 
 val interp_modexpr : env -> module_ast -> module_struct_entry
 
-(* The following function tries to interprete an ast as a module,
+(** The following function tries to interprete an ast as a module,
    and in case of failure, interpretes this ast as a module type.
    The boolean is true for a module, false for a module type *)
 
diff --git a/interp/notation.mli b/interp/notation.mli
index f52e17cc8..91f262b48 100644
--- a/interp/notation.mli
+++ b/interp/notation.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 Bigint
@@ -19,18 +18,19 @@ open Rawterm
 open Topconstr
 open Ppextend
 
-(*i*)
+(**/**)
 
-(**********************************************************************)
-(* Scopes *)
+(*********************************************************************
+   Scopes *)
 
-(*s A scope is a set of interpreters for symbols + optional
+(** {6 Sect } *)
+(** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
 type level = precedence * tolerability list
 type delimiters = string
 type scope
-type scopes (* = [scope_name list] *)
+type scopes (** = [scope_name list] *)
 
 type local_scopes = tmp_scope_name option * scope_name list
 
@@ -39,35 +39,35 @@ val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
 
-(* Check where a scope is opened or not in a scope list, or in
+(** Check where a scope is opened or not in a scope list, or in
  * the current opened scopes *)
 val scope_is_open_in_scopes : scope_name -> scopes -> bool
 val scope_is_open : scope_name -> bool
 
-(* Open scope *)
+(** Open scope *)
 
 val open_close_scope :
-  (* locality *) bool * (* open *) bool * scope_name -> unit
+  (** locality *) bool * (* open *) bool * scope_name -> unit
 
-(* Extend a list of scopes *)
+(** Extend a list of scopes *)
 val empty_scope_stack : scopes
 val push_scope : scope_name -> scopes -> scopes
 
-(* Declare delimiters for printing *)
+(** Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
 val find_delimiters_scope : loc -> delimiters -> scope_name
 
-(*s Declare and uses back and forth an interpretation of primitive token *)
+(** {6 Declare and uses back and forth an interpretation of primitive token } *)
 
-(* A numeral interpreter is the pair of an interpreter for **integer**
+(** A numeral interpreter is the pair of an interpreter for **integer**
    numbers in terms and an optional interpreter in pattern, if
    negative numbers are not supported, the interpreter must fail with
    an appropriate error message *)
 
 type notation_location = (dir_path * dir_path) * string
 type required_module = full_path * string list
-type cases_pattern_status = bool (* true = use prim token in patterns *)
+type cases_pattern_status = bool (** true = use prim token in patterns *)
 
 type 'a prim_token_interpreter =
     loc -> 'a -> rawconstr
@@ -81,7 +81,7 @@ val declare_numeral_interpreter : scope_name -> required_module ->
 val declare_string_interpreter : scope_name -> required_module ->
   string prim_token_interpreter -> string prim_token_uninterpreter -> unit
 
-(* Return the [term]/[cases_pattern] bound to a primitive token in a
+(** Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
 
 val interp_prim_token : loc -> prim_token -> local_scopes ->
@@ -89,7 +89,7 @@ val interp_prim_token : loc -> prim_token -> local_scopes ->
 val interp_prim_token_cases_pattern : loc -> prim_token -> name ->
   local_scopes -> cases_pattern * (notation_location * scope_name option)
 
-(* Return the primitive token associated to a [term]/[cases_pattern];
+(** Return the primitive token associated to a [term]/[cases_pattern];
    raise [No_match] if no such token *)
 
 val uninterp_prim_token :
@@ -100,9 +100,9 @@ val uninterp_prim_token_cases_pattern :
 val availability_of_prim_token :
   prim_token -> scope_name -> local_scopes -> delimiters option option
 
-(*s Declare and interpret back and forth a notation *)
+(** {6 Declare and interpret back and forth a notation } *)
 
-(* Binds a notation in a given scope to an interpretation *)
+(** Binds a notation in a given scope to an interpretation *)
 type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of kernel_name
@@ -112,39 +112,39 @@ val declare_notation_interpretation : notation -> scope_name option ->
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
-(* Return the interpretation bound to a notation *)
+(** Return the interpretation bound to a notation *)
 val interp_notation : loc -> notation -> local_scopes ->
       interpretation * (notation_location * scope_name option)
 
-(* Return the possible notations for a given term *)
+(** Return the possible notations for a given term *)
 val uninterp_notations : rawconstr ->
       (interp_rule * interpretation * int option) list
 val uninterp_cases_pattern_notations : cases_pattern ->
       (interp_rule * interpretation * int option) list
 
-(* Test if a notation is available in the scopes *)
-(* context [scopes]; if available, the result is not None; the first *)
-(* argument is itself not None if a delimiters is needed *)
+(** Test if a notation is available in the scopes 
+   context [scopes]; if available, the result is not None; the first 
+   argument is itself not None if a delimiters is needed *)
 val availability_of_notation : scope_name option * notation -> local_scopes ->
   (scope_name option * delimiters option) option
 
-(*s Declare and test the level of a (possibly uninterpreted) notation *)
+(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
 val declare_notation_level : notation -> level -> unit
-val level_of_notation : notation -> level (* raise [Not_found] if no level *)
+val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 
 (*s** Miscellaneous *)
 
 val interp_notation_as_global_reference : loc -> (global_reference -> bool) ->
       notation -> delimiters option -> global_reference
 
-(* Checks for already existing notations *)
+(** Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
       interpretation -> bool
 
-(* Declares and looks for scopes associated to arguments of a global ref *)
+(** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
-  bool (* true=local *) -> global_reference -> scope_name option list -> unit
+  bool (** true=local *) -> global_reference -> scope_name option list -> unit
 
 val find_arguments_scope : global_reference -> scope_name option list
 
@@ -153,7 +153,7 @@ val declare_ref_arguments_scope : global_reference -> unit
 
 val compute_arguments_scope : Term.types -> scope_name option list
 
-(* Building notation key *)
+(** Building notation key *)
 
 type symbol =
   | Terminal of string
@@ -164,7 +164,7 @@ type symbol =
 val make_notation_key : symbol list -> notation
 val decompose_notation_key : notation -> symbol list
 
-(* Prints scopes (expects a pure aconstr printer) *)
+(** Prints scopes (expects a pure aconstr printer) *)
 val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
 val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
 val locate_notation : (rawconstr -> std_ppcmds) -> notation ->
@@ -172,13 +172,13 @@ val locate_notation : (rawconstr -> std_ppcmds) -> notation ->
 
 val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
 
-(**********************************************************************)
-(*s Printing rules for notations *)
+(*********************************************************************
+  s Printing rules for notations *)
 
-(* Declare and look for the printing rule for symbolic notations *)
+(** Declare and look for the printing rule for symbolic notations *)
 type unparsing_rule = unparsing list * precedence
 val declare_notation_printing_rule : notation -> unparsing_rule -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
 
-(**********************************************************************)
-(* Rem: printing rules for primitive token are canonical *)
+(*********************************************************************
+   Rem: printing rules for primitive token are canonical *)
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 3d09587d0..984696cda 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -1,21 +1,19 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
+(***********************************************************************
+    v      *   The Coq Proof Assistant  /  The Coq Development Team     
+   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
+     \VV/  *************************************************************
+      //   *      This file is distributed under the terms of the       
+           *       GNU Lesser General Public License Version 2.1        
+  ***********************************************************************)
 
 (*i $Id$ i*)
 
-(*i*)
 open Pp
 open Names
-(*i*)
 
-(*s Pretty-print. *)
+(** {6 Pretty-print. } *)
 
-(* Dealing with precedences *)
+(** Dealing with precedences *)
 
 type precedence = int
 
diff --git a/interp/reserve.mli b/interp/reserve.mli
index a83e66c4a..4cc2eff5a 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.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/interp/smartlocate.mli b/interp/smartlocate.mli
index 682484f57..b505e7db7 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -1,37 +1,37 @@
-(************************************************************************)
-(*  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:{% $ %} *)
 
 open Util
 open Names
 open Libnames
 open Genarg
 
-(* [locate_global_with_alias] locates global reference possibly following
+(** [locate_global_with_alias] locates global reference possibly following
    a notation if this notation has a role of aliasing; raise Not_found
    if not bound in the global env; raise an error if bound to a
    syntactic def that does not denote a reference *)
 
 val locate_global_with_alias : qualid located -> global_reference
 
-(* Extract a global_reference from a reference that can be an "alias" *)
+(** Extract a global_reference from a reference that can be an "alias" *)
 val global_of_extended_global : extended_global_reference -> global_reference
 
-(* Locate a reference taking into account possible "alias" notations *)
+(** Locate a reference taking into account possible "alias" notations *)
 val global_with_alias : reference -> global_reference
 
-(* The same for inductive types *)
+(** The same for inductive types *)
 val global_inductive_with_alias : reference -> inductive
 
-(* Locate a reference taking into account notations and "aliases" *)
+(** Locate a reference taking into account notations and "aliases" *)
 val smart_global : reference or_by_notation -> global_reference
 
-(* The same for inductive types *)
+(** The same for inductive types *)
 val smart_global_inductive : reference or_by_notation -> inductive
 
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index b4da6dd7a..6b57b497a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.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 Util
 open Names
 open Topconstr
 open Rawterm
 open Nametab
 open Libnames
-(*i*)
 
-(* Syntactic definitions. *)
+(** Syntactic definitions. *)
 
 type syndef_interpretation = (identifier * subscopes) list * aconstr
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 2f25be94c..02e6d1eeb 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.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
@@ -16,20 +15,20 @@ open Libnames
 open Rawterm
 open Term
 open Mod_subst
-(*i*)
 
-(*s This is the subtype of rawconstr allowed in syntactic extensions *)
-(* No location since intended to be substituted at any place of a text *)
-(* Complex expressions such as fixpoints and cofixpoints are excluded, *)
-(* non global expressions such as existential variables also *)
+(** {6 Sect } *)
+(** This is the subtype of rawconstr allowed in syntactic extensions 
+   No location since intended to be substituted at any place of a text 
+   Complex expressions such as fixpoints and cofixpoints are excluded, 
+   non global expressions such as existential variables also *)
 
 type aconstr =
-  (* Part common to [rawconstr] and [cases_pattern] *)
+  (** Part common to [rawconstr] and [cases_pattern] *)
   | ARef of global_reference
   | AVar of identifier
   | AApp of aconstr * aconstr list
   | AList of identifier * identifier * aconstr * aconstr * bool
-  (* Part only in [rawconstr] *)
+  (** Part only in [rawconstr] *)
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
@@ -46,20 +45,20 @@ type aconstr =
   | APatVar of patvar
   | ACast of aconstr * aconstr cast_type
 
-(**********************************************************************)
-(* Translate a rawconstr into a notation given the list of variables  *)
-(* bound by the notation; also interpret recursive patterns           *)
+(*********************************************************************
+   Translate a rawconstr into a notation given the list of variables  
+   bound by the notation; also interpret recursive patterns           *)
 
 val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr
 
-(* Name of the special identifier used to encode recursive notations  *)
+(** Name of the special identifier used to encode recursive notations  *)
 val ldots_var : identifier
 
-(* Equality of rawconstr (warning: only partially implemented) *)
+(** Equality of rawconstr (warning: only partially implemented) *)
 val eq_rawconstr : rawconstr -> rawconstr -> bool
 
-(**********************************************************************)
-(* Re-interpret a notation as a rawconstr, taking care of binders     *)
+(*********************************************************************
+   Re-interpret a notation as a rawconstr, taking care of binders     *)
 
 val rawconstr_of_aconstr_with_binders : loc ->
   ('a -> name -> 'a * name) ->
@@ -67,9 +66,9 @@ val rawconstr_of_aconstr_with_binders : loc ->
 
 val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
 
-(**********************************************************************)
-(* [match_aconstr metas] matches a rawconstr against an aconstr with  *)
-(* metavariables in [metas]; raise [No_match] if the matching fails   *)
+(*********************************************************************
+   [match_aconstr metas] matches a rawconstr against an aconstr with  
+   metavariables in [metas]; raise [No_match] if the matching fails   *)
 
 exception No_match
 
@@ -80,19 +79,19 @@ type tmp_scope_name = scope_name
 type subscopes = tmp_scope_name option * scope_name list
 
 type interpretation =
-    (* regular vars of notation    / recursive parts of notation    / body *)
+    (** regular vars of notation    / recursive parts of notation    / body *)
     ((identifier * subscopes) list * (identifier * subscopes) list) * aconstr
 
 val match_aconstr : rawconstr -> interpretation ->
       (rawconstr * subscopes) list * (rawconstr list * subscopes) list
 
-(**********************************************************************)
-(* Substitution of kernel names in interpretation data                *)
+(*********************************************************************
+   Substitution of kernel names in interpretation data                *)
 
 val subst_interpretation : substitution -> interpretation -> interpretation
 
-(**********************************************************************)
-(*s Concrete syntax for terms                                         *)
+(*********************************************************************
+  s Concrete syntax for terms                                         *)
 
 type notation = string
 
@@ -101,17 +100,17 @@ type explicitation = ExplByPos of int * identifier option | ExplByName of identi
 type binder_kind =
   | Default of binding_kind
   | Generalized of binding_kind * binding_kind * bool
-      (* Inner binding, outer bindings, typeclass-specific flag
+      (** Inner binding, outer bindings, typeclass-specific flag
 	 for implicit generalization of superclasses *)
 
 type abstraction_kind = AbsLambda | AbsPi
 
-type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
+type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
 type prim_token = Numeral of Bigint.bigint | String of string
 
 type 'a notation_substitution =
-    'a list * (* for recursive notations: *) 'a list list
+    'a list * (** for recursive notations: *) 'a list list
 
 type cases_pattern_expr =
   | CPatAlias of loc * cases_pattern_expr * identifier
@@ -162,7 +161,7 @@ and cofix_expr =
 and recursion_order_expr =
   | CStructRec
   | CWfRec of constr_expr
-  | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
+  | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
 
 (** Anonymous defs allowed ?? *)
 and local_binder =
@@ -175,8 +174,8 @@ and typeclass_context = typeclass_constraint list
 
 type constr_pattern_expr = constr_expr
 
-(**********************************************************************)
-(* Utilities on constr_expr                                           *)
+(*********************************************************************
+   Utilities on constr_expr                                           *)
 
 val constr_loc : constr_expr -> loc
 
@@ -190,7 +189,7 @@ val occur_var_constr_expr : identifier -> constr_expr -> bool
 
 val default_binder_kind : binder_kind
 
-(* Specific function for interning "in indtype" syntax of "match" *)
+(** Specific function for interning "in indtype" syntax of "match" *)
 val ids_of_cases_indtype : constr_expr -> identifier list
 
 val mkIdentC : identifier -> constr_expr
@@ -210,32 +209,32 @@ val index_of_annot : local_binder list -> identifier located option -> int optio
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 
-(* Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
+(** Same as [abstract_constr_expr] and [prod_constr_expr], with location *)
 val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr
 val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr
 
-(* For binders parsing *)
+(** For binders parsing *)
 
-(* With let binders *)
+(** With let binders *)
 val names_of_local_binders : local_binder list -> name located list
 
-(* Does not take let binders into account *)
+(** Does not take let binders into account *)
 val names_of_local_assums : local_binder list -> name located list
 
-(* Used in typeclasses *)
+(** Used in typeclasses *)
 
 val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
    ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
 
-(* Used in correctness and interface; absence of var capture not guaranteed *)
-(* in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
+(** Used in correctness and interface; absence of var capture not guaranteed 
+   in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
 
 val map_constr_expr_with_binders :
   (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
       'a -> constr_expr -> constr_expr
 
-(**********************************************************************)
-(* Concrete syntax for modules and module types                       *)
+(*********************************************************************
+   Concrete syntax for modules and module types                       *)
 
 type with_declaration_ast =
   | CWith_Module of identifier list located * qualid located
@@ -246,11 +245,11 @@ type module_ast =
   | CMapply of module_ast * module_ast
   | CMwith of module_ast * with_declaration_ast
 
-type module_ast_inl = module_ast * bool (* honor the inline annotations or not *)
+type module_ast_inl = module_ast * bool (** honor the inline annotations or not *)
 
 type 'a module_signature =
-  | Enforce of 'a (* ... : T *)
-  | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
+  | Enforce of 'a (** ... : T *)
+  | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
 
 val ntn_loc :
   Util.loc -> constr_expr notation_substitution -> string -> (int * int) list