Various minor improvements of comments in mli for ocamldoc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7

44 files changed, 194 insertions, 194 deletions

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index bf28e0850..880f8a4be 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -18,19 +18,17 @@ open Topconstr
 open Termops
 open Pretyping
 
-(** {6 Sect } *)
-(** Translation from front abstract syntax of term to untyped terms (rawconstr)
+(** Translation from front abstract syntax of term to untyped terms (rawconstr) *)
 
-   The translation performs:
+(** The translation performs:
 
    - resolution of names :
       - check all variables are bound
       - make absolute the references to global objets
    - resolution of symbolic notations using scopes
    - 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.
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index a80e749d3..1d7f571b3 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -12,11 +12,10 @@ open Nametab
 open Term
 open Pattern
 
-(** {6 Sect } *)
 (** This module collects the global references, constructions and
     patterns of the standard library used in ocaml files *)
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [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
@@ -80,7 +79,7 @@ val glob_eq : global_reference
 val glob_identity : global_reference
 val glob_jmeq : global_reference
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** 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
@@ -144,7 +143,7 @@ val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 (** Specif *)
 val build_coq_sumbool : constr delayed
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Connectives 
    The False proposition *)
 val build_coq_False : constr delayed
diff --git a/interp/notation.mli b/interp/notation.mli
index 224fb1d45..3da9ec0e5 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -16,12 +16,9 @@ open Rawterm
 open Topconstr
 open Ppextend
 
-(**/**)
+(** Notations *)
 
-(*********************************************************************
-   Scopes *)
-
-(** {6 Sect } *)
+(** {6 Scopes } *)
 (** A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
@@ -131,7 +128,7 @@ val availability_of_notation : scope_name option * notation -> local_scopes ->
 val declare_notation_level : notation -> level -> unit
 val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 
-(*s** Miscellaneous *)
+(** {6 Miscellaneous} *)
 
 val interp_notation_as_global_reference : loc -> (global_reference -> bool) ->
       notation -> delimiters option -> global_reference
@@ -170,13 +167,11 @@ val locate_notation : (rawconstr -> std_ppcmds) -> notation ->
 
 val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
 
-(*********************************************************************
-  s Printing rules for notations *)
+(** {6 Printing rules for 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/topconstr.mli b/interp/topconstr.mli
index 2b9506747..8f1fa5c3d 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -14,7 +14,9 @@ open Rawterm
 open Term
 open Mod_subst
 
-(** {6 Sect } *)
+(** Topconstr: definitions of [aconstr] et [constr_expr] *)
+
+(** {6 aconstr } *)
 (** 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, 
@@ -43,9 +45,8 @@ 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
 
@@ -55,8 +56,7 @@ val ldots_var : identifier
 (** 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) ->
@@ -64,8 +64,7 @@ val rawconstr_of_aconstr_with_binders : loc ->
 
 val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
 
-(*********************************************************************
-   [match_aconstr metas] matches a rawconstr against an aconstr with  
+(** [match_aconstr metas] matches a rawconstr against an aconstr with
    metavariables in [metas]; raise [No_match] if the matching fails   *)
 
 exception No_match
@@ -83,13 +82,11 @@ type interpretation =
 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                                         *)
+(** {6 Concrete syntax for terms }                                        *)
 
 type notation = string
 
@@ -172,8 +169,7 @@ 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
 
@@ -231,8 +227,7 @@ 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
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 547155423..a8ecc82b4 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -8,7 +8,7 @@ type reloc_info =
 
 type patch = reloc_info * int
 
-(** A virer *)
+(* A virer *)
 val subst_patch : Mod_subst.substitution -> patch -> patch
 
 type emitcodes
diff --git a/kernel/closure.mli b/kernel/closure.mli
index d482e91b2..9a8ced44e 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -18,7 +18,7 @@ val share : bool ref
 
 val with_stats: 'a Lazy.t -> 'a
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Delta implies all consts (both global (= by
   [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0ecfa21b6..8c31742f3 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -120,7 +120,7 @@ val add_constant : constant -> constant_body -> env -> env
 val lookup_constant    : constant -> env -> constant_body
 val evaluable_constant : constant -> env -> bool
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [constant_value env c] raises [NotEvaluableConst Opaque] if
    [c] is opaque and [NotEvaluableConst NoBody] if it has no
    body and [Not_found] if it does not exist in [env] *)
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index fd7753093..dd7096c4b 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -6,13 +6,15 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(** {6 Sect } *)
+(** Explicit substitutions *)
+
+(** {6 Explicit substitutions } *)
 (** Explicit substitutions of type ['a]. 
     - ESID(n)             = %n END   bounded identity
- *  - CONS([|t1..tn|],S)  = (S.t1...tn)    parallel substitution
- *       (beware of the order: indice 1 is substituted by tn)
- *  - SHIFT(n,S)          = (^n o S) terms in S are relocated with n vars
- *  - LIFT(n,S)           = (%n S) stands for ((^n o S).n...1)
+    - CONS([|t1..tn|],S)  = (S.t1...tn)    parallel substitution
+        (beware of the order: indice 1 is substituted by tn)
+    - SHIFT(n,S)          = (^n o S) terms in S are relocated with n vars
+    - LIFT(n,S)           = (%n S) stands for ((^n o S).n...1)
          (corresponds to S crossing n binders) *)
 type 'a subs =
   | ESID of int
@@ -30,28 +32,28 @@ val subs_liftn: int -> 'a subs -> 'a subs
 val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
 
 (** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
- * [subs]. The result is either (Inl(lams,v)) when the variable is
- * substituted by value [v] under lams binders (i.e. v *has* to be
- * shifted by lams), or (Inr (k',p)) when the variable k is just relocated
- * as k'; p is None if the variable points inside subs and Some(k) if the
- * variable points k bindings beyond subs (cf argument of ESID).
- *)
+    [subs]. The result is either (Inl(lams,v)) when the variable is
+    substituted by value [v] under lams binders (i.e. v *has* to be
+    shifted by lams), or (Inr (k',p)) when the variable k is just relocated
+    as k'; p is None if the variable points inside subs and Some(k) if the
+    variable points k bindings beyond subs (cf argument of ESID).
+*)
 val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
 
 (** Tests whether a substitution behaves like the identity *)
 val is_subs_id: 'a subs -> bool
 
 (** Composition of substitutions: [comp mk_clos s1 s2] computes a
- * substitution equivalent to applying s2 then s1. Argument
- * mk_clos is used when a closure has to be created, i.e. when
- * s1 is applied on an element of s2.
- *)
+    substitution equivalent to applying s2 then s1. Argument
+    mk_clos is used when a closure has to be created, i.e. when
+    s1 is applied on an element of s2.
+*)
 val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
 
-(** {6 Sect } *)
-(** Compact representation of explicit relocations. \\
-   [ELSHFT(l,n)] == lift of [n], then apply [lift l].
-   [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
+(** {6 Compact representation } *)
+(** Compact representation of explicit relocations
+    - [ELSHFT(l,n)] == lift of [n], then apply [lift l].
+    - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
 type lift =
   | ELID
   | ELSHFT of lift * int
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 388eb21e4..a3867c6b8 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -14,8 +14,8 @@ open Environ
 open Entries
 open Typeops
 
+(** Inductive type checking and errors *)
 
-(** {6 Sect } *)
 (** The different kinds of errors that may result of a malformed inductive
   definition. *)
 
@@ -34,7 +34,7 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
-(** {6 The following function does checks on inductive declarations. } *)
+(** The following function does checks on inductive declarations. *)
 
 val check_inductive :
   env -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 259e1decd..3212b8eed 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -26,7 +26,7 @@ val find_coinductive : env -> types -> inductive * constr list
 
 type mind_specif = mutual_inductive_body * one_inductive_body
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Fetching information in the environment about an inductive type.
     Raises [Not_found] if the inductive type is not found. *)
 val lookup_mind_specif : env -> inductive -> mind_specif
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index e22a3eb7d..2514e409c 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -90,7 +90,8 @@ val from_val : 'a -> 'a substituted
 val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
 val subst_substituted : substitution -> 'a substituted -> 'a substituted
 
-(*i debugging *)
+(**/**)
+(* debugging *)
 val debug_string_of_subst : substitution -> string
 val debug_pr_subst : substitution -> Pp.std_ppcmds
 val debug_string_of_delta : delta_resolver -> string
diff --git a/kernel/names.mli b/kernel/names.mli
index ffbc02714..1c74fdee6 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -39,7 +39,7 @@ val empty_dirpath : dir_path
 val string_of_dirpath : dir_path -> string
 
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Unique identifier to be used as "self" in structures and
   signatures - invisible for users *)
 type label
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ce62eeafc..3e1051088 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -12,8 +12,9 @@ open Declarations
 open Entries
 open Mod_subst
 
-(** {6 Sect } *)
-(** Safe environments. Since we are now able to type terms, we can
+(** {6 Safe environments } *)
+
+(** Since we are now able to type terms, we can
   define an abstract type of safe environments, where objects are
   typed before being added.
 
@@ -69,6 +70,7 @@ val set_engagement : engagement -> safe_environment -> safe_environment
 
 
 (** {6 Interactive module functions } *)
+
 val start_module :
   label -> safe_environment -> module_path * safe_environment
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 07f3df19e..ddb88287e 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -34,7 +34,7 @@ val fold_named_context_reverse :
 (** {6 Section-related auxiliary functions } *)
 val instance_from_named_context : named_context -> constr array
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 3940d74c5..f7819d6e6 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -64,7 +64,7 @@ val eq_constr : constr -> constr -> bool
 
 type types = constr
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Functions for dealing with constr terms.
   The following functions are intended to simplify and to uniform the
   manipulation of terms. Some of these functions may be overlapped with
@@ -253,7 +253,7 @@ val is_Type : constr -> bool
 val iskind : constr -> bool
 val is_small : sorts -> bool
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Term destructors.
    Destructor operations are partial functions and
    raise [invalid_arg "dest*"] if the term has not the expected form. *)
@@ -319,7 +319,7 @@ val destFix : constr -> fixpoint
 val destCoFix : constr -> cofixpoint
 
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** A {e declaration} has the form (name,body,type). It is either an
     {e assumption} if [body=None] or a {e definition} if
     [body=Some actualbody]. It is referred by {e name} if [na] is an
@@ -483,7 +483,7 @@ val under_casts : (constr -> constr) -> constr -> constr
 (** Apply a function under components of Cast if any *)
 val under_outer_cast : (constr -> constr) -> constr -> constr
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
     Such a term can canonically be seen as the pair of a context of types
     and of a sort *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3a2ec557f..1634009b3 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -51,7 +51,7 @@ type constraint_function = universe -> universe -> constraints -> constraints
 val enforce_geq : constraint_function
 val enforce_eq : constraint_function
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Merge of constraints in a universes graph.
   The function [merge_constraints] merges a set of constraints in a given
   universes graph. It raises the exception [UniverseInconsistency] if the
diff --git a/kernel/vm.mli b/kernel/vm.mli
index ff76e7cd5..cd5999f04 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -3,16 +3,18 @@ open Term
 open Cbytecodes
 open Cemitcodes
 
+(** Efficient Virtual Machine *)
 
 val set_drawinstr : unit -> unit
 
 val transp_values : unit -> bool
 val set_transp_values : bool -> unit
 
-(** le code machine *)
+(** Machine code *)
+
 type tcode
 
-(** Les valeurs ***********)
+(** Values *)
 
 type vprod
 type vfun
@@ -27,11 +29,11 @@ type atom =
   | Aiddef of id_key * values
   | Aind of inductive
 
-(** Les zippers *)
+(** Zippers *)
 
 type zipper =
   | Zapp of arguments
-  | Zfix of vfix*arguments  (** Peut-etre vide *)
+  | Zfix of vfix * arguments  (** might be empty *)
   | Zswitch of vswitch
 
 type stack = zipper list
@@ -49,6 +51,7 @@ type whd =
   | Vatom_stk of atom * stack
 
 (** Constructors *)
+
 val val_of_str_const : structured_constant -> values
 
 val val_of_rel : int -> values
@@ -63,21 +66,26 @@ val val_of_constant_def : int -> constant -> values -> values
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
 (** Destructors *)
+
 val whd_val : values -> whd
 
 (** Arguments *)
+
 val nargs : arguments -> int
 val arg : arguments -> int -> values
 
 (** Product *)
+
 val dom : vprod -> values
 val codom : vprod -> vfun
 
 (** Function *)
+
 val body_of_vfun : int -> vfun -> values
 val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
 
 (** Fix *)
+
 val current_fix : vfix -> int
 val check_fix : vfix -> vfix -> bool
 val rec_args : vfix -> int array
@@ -85,22 +93,27 @@ val reduce_fix : int -> vfix -> vfun array * values array
                               (** bodies ,  types *)
 
 (** CoFix *)
+
 val current_cofix : vcofix -> int
 val check_cofix : vcofix -> vcofix -> bool
 val reduce_cofix : int -> vcofix -> values array * values array
-                                      (** bodies , types 
-   Block *)
+                                      (** bodies , types *)
+
+(** Block *)
+
 val btag : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values
 
 (** Switch *)
+
 val check_switch : vswitch -> vswitch -> bool
 val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
 (** Evaluation *)
+
 val whd_stack : values -> stack -> whd
 val force_whd : values -> stack -> whd
 
diff --git a/lib/explore.mli b/lib/explore.mli
index 0e8eb32be..1f17f8a4c 100644
--- a/lib/explore.mli
+++ b/lib/explore.mli
@@ -8,7 +8,7 @@
 
 (** {6 Search strategies. } *)
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** A search problem implements the following signature [SearchProblem].
     [state] is the type of states of the search tree.
     [branching] is the branching function; if [branching s] returns an
@@ -31,7 +31,7 @@ module type SearchProblem = sig
 
 end
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Functor [Make] returns some search functions given a search problem.
     Search functions raise [Not_found] if no success is found.
     States are always visited in the order they appear in the
diff --git a/lib/pp.mli b/lib/pp.mli
index 56e66225c..ca62f82d6 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -89,7 +89,7 @@ val msg_with : Format.formatter -> std_ppcmds -> unit
 val msgnl_with : Format.formatter -> std_ppcmds -> unit
 
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** The following functions are instances of the previous ones on
   [std_ft] and [err_ft]. *)
 
diff --git a/lib/system.mli b/lib/system.mli
index 09142f365..d8a4088d0 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -6,12 +6,14 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(** {6 Sect } *)
-(** Files and load paths. Load path entries remember the original root
+(** System utilities *)
+
+(** {6 Files and load paths} *)
+
+(** Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
     [directory]), the root path and the path relative to the root. *)
 
-
 type physical_path = string
 type load_path = physical_path list
 
@@ -38,7 +40,7 @@ val exists_dir : string -> bool
 val find_file_in_path :
   ?warn:bool -> load_path -> string -> physical_path * string
 
-(** {6 Sect } *)
+(** {6 I/O functions } *)
 (** Generic input and output functions, parameterized by a magic number
   and a suffix. The intern functions raise the exception [Bad_magic_number]
   when the check fails, with the full file name. *)
@@ -58,7 +60,7 @@ val extern_intern : ?warn:bool -> int -> string ->
 
 val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
 
-(** {6 Sect } *)
+(** {6 Executing commands } *)
 (** [run_command converter f com] launches command [com], and returns
     the contents of stdout and stderr that have been processed with
     [converter]; the processed contents of stdout and stderr is also
diff --git a/lib/util.mli b/lib/util.mli
index fd8ff9275..f7f40b805 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -11,7 +11,7 @@ open Pp
 (** This module contains numerous utility functions on strings, lists,
    arrays, etc. *)
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Errors. [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
@@ -361,7 +361,7 @@ val size_kb : 'a -> int
 val heap_size : unit -> int
 val heap_size_kb : unit -> int
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)
 
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 4cbdf4ce4..b7126147e 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -13,9 +13,7 @@ open Environ
 open Libnames
 open Libobject
 open Lib
-   (**/**)
 
-(** {6 Sect } *)
 (** This modules provides official functions to declare modules and
   module types *)
 
@@ -65,7 +63,7 @@ val start_modtype : (env -> 'modast -> module_struct_entry) ->
 val end_modtype : unit -> module_path
 
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Objects of a module. They come in two lists: the substitutive ones
   and the other *)
 
@@ -107,7 +105,7 @@ val import_module : bool -> module_path -> unit
 val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) ->
   ('struct_expr * bool) list -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [iter_all_segments] iterate over all segments, the modules'
     segments first and then the current segment. Modules are presented
     in an arbitrary order. The given function is applied to all leaves
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
index b264c1228..98e3d93d5 100644
--- a/library/dischargedhypsmap.mli
+++ b/library/dischargedhypsmap.mli
@@ -13,7 +13,6 @@ open Nametab
 
 type discharged_hyps = full_path list
 
-(** {6 Sect } *)
 (** Discharged hypothesis. Here we store the discharged hypothesis of each 
     constant or inductive type declaration.                                *)
 
diff --git a/library/global.mli b/library/global.mli
index ae2ed16f7..d29aca5d3 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -14,7 +14,6 @@ open Entries
 open Indtypes
 open Mod_subst
 open Safe_typing
-   (**/**)
 
 (** This module defines the global environment of Coq.  The functions
    below are exactly the same as the ones in [Safe_typing], operating on
@@ -39,7 +38,7 @@ val env_is_empty : unit -> bool
 val push_named_assum : (identifier * types) -> Univ.constraints
 val push_named_def   : (identifier * constr * types option) -> Univ.constraints
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Adding constants, inductives, modules and module types.  All these
   functions verify that given names match those generated by kernel *)
 
@@ -94,7 +93,7 @@ val start_library : dir_path -> module_path
 val export : dir_path -> module_path * compiled_library
 val import : compiled_library -> Digest.t -> module_path
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Function to get an environment from the constants part of the global
  * environment and a given context. *)
 
diff --git a/library/impargs.mli b/library/impargs.mli
index f43880e29..2eab1af66 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -12,8 +12,10 @@ open Term
 open Environ
 open Nametab
 
-(** {6 Sect } *)
-(** Implicit arguments. Here we store the implicit arguments. Notice that we
+(** Implicit Arguments *)
+
+(** {6 ... } *)
+(** Here we store the implicit arguments. Notice that we
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
@@ -33,7 +35,7 @@ val is_maximal_implicit_args : unit -> bool
 type implicits_flags
 val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** An [implicits_list] is a list of positions telling which arguments
     of a reference can be automatically infered *)
 
diff --git a/library/lib.mli b/library/lib.mli
index f1e64e69a..5fb65a41f 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -7,7 +7,8 @@
   ***********************************************************************)
 
 
-(** {6 Sect } *)
+(** Lib: record of operations, backtrack, low-level sections *)
+
 (** This module provides a general mechanism to keep a trace of all operations
    and to backtrack (undo) those operations. It provides also the section
    mechanism (at a low level; discharge is not known at this step). *)
@@ -27,7 +28,7 @@ and library_segment = (Libnames.object_name * node) list
 
 type lib_objects = (Names.identifier * Libobject.obj) list
 
-(** {6 Object iteratation functions. } *)
+(** {6 Object iteration functions. } *)
 
 val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
 val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
@@ -47,7 +48,7 @@ val segment_of_objects :
   Libnames.object_prefix -> lib_objects -> library_segment
 
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
@@ -71,7 +72,7 @@ val current_command_label : unit -> int
    registered after it. *)
 val reset_label : int -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** The function [contents_after] returns the current library segment,
   starting from a given section path. If not given, the entire segment
   is returned. *)
diff --git a/library/libnames.mli b/library/libnames.mli
index 9db6d787d..4e9ddcb56 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -120,7 +120,7 @@ val encode_con : dir_path -> identifier -> constant
 val decode_con : constant -> dir_path * identifier
 
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** A [qualid] is a partially qualified ident; it includes fully
     qualified names (= absolute names) and all intermediate partial
     qualifications of absolute names, including single identifiers.
@@ -161,7 +161,7 @@ type global_dir_reference =
   | DirClosedSection of dir_path
       (** this won't last long I hope! *)
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** A [reference] is the user-level notion of name. It denotes either a
     global name (referred either by a qualified name or by a single
     name) or a variable *)
diff --git a/library/libobject.mli b/library/libobject.mli
index 5a48419c9..87bbbe89d 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -84,7 +84,7 @@ val default_object : string -> 'a object_declaration
 (** the identity substitution function *)
 val ident_subst_function : substitution * 'a -> 'a
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Given an object declaration, the function [declare_object]
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
diff --git a/library/library.mli b/library/library.mli
index 9bbb45143..87e376ab9 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -11,7 +11,6 @@ open Names
 open Libnames
 open Libobject
 
-(** {6 Sect } *)
 (** This module provides functions to load, open and save
   libraries. Libraries correspond to the subclass of modules that
   coincide with a file on disk (the ".vo" files). Libraries on the
@@ -20,7 +19,7 @@ open Libobject
   written at various dates.
 *)
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library : qualid located list -> bool option -> unit
@@ -28,7 +27,7 @@ val require_library_from_dirpath : (dir_path * string) list -> bool option -> un
 val require_library_from_file :
   identifier option -> System.physical_path -> bool option -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located -> unit
@@ -58,7 +57,7 @@ val overwrite_library_filenames : string -> unit
 (** {6 Hook for the xml exportation of libraries } *)
 val set_xml_require : (dir_path -> unit) -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Global load paths: a load path is a physical path in the file
     system; to each load path is associated a Coq [dir_path] (the "logical"
     path of the physical path) *)
diff --git a/library/nametab.mli b/library/nametab.mli
index a464fd9a9..4303d86a3 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -11,51 +11,48 @@ open Pp
 open Names
 open Libnames
 
-(** {6 Sect } *)
-(** This module contains the tables for globalization, which
-    associates internal object references to qualified names (qualid).
+(** This module contains the tables for globalization. *)
 
-    There are three classes of names:
+(** These globalization tables associate internal object references to
+    qualified names (qualid). There are three classes of names:
 
-    1a- internal kernel names: [kernel_name], [constant], [inductive],
-        [module_path], [dir_path]
+    - 1a) internal kernel names: [kernel_name], [constant], [inductive],
+         [module_path], [dir_path]
 
-    1b- other internal names: [global_reference], [syndef_name],
+    - 1b) other internal names: [global_reference], [syndef_name],
         [extended_global_reference], [global_dir_reference], ...
 
-    2- full, non ambiguous user names: [full_path]
+    - 2) full, non ambiguous user names: [full_path]
 
-    3- non necessarily full, possibly ambiguous user names: [reference]
-       and [qualid]
+    - 3) non necessarily full, possibly ambiguous user names: [reference]
+        and [qualid]
 *)
 
 (** Most functions in this module fall into one of the following categories:
-   {% \begin{%}itemize{% }%}
-   \item [push : visibility -> full_user_name -> object_reference -> unit]
-
-   Registers the [object_reference] to be referred to by the
-   [full_user_name] (and its suffixes according to [visibility]).
-   [full_user_name] can either be a [full_path] or a [dir_path].
-
-   \item [exists : full_user_name -> bool]
-
-   Is the [full_user_name] already atributed as an absolute user name
-   of some object?
-
-   \item [locate : qualid -> object_reference]
-
-   Finds the object referred to by [qualid] or raises [Not_found]
-
-   \item [full_name : qualid -> full_user_name]
-
-   Finds the full user name referred to by [qualid] or raises [Not_found]
-
-   \item [shortest_qualid_of : object_reference -> user_name]
-
-   The [user_name] can be for example the shortest non ambiguous [qualid] or
-   the [full_user_name] or [identifier]. Such a function can also have a
-   local context argument.
-   {% \end{%}itemize{% }%}
+{ul {- [push : visibility -> full_user_name -> object_reference -> unit]
+
+     Registers the [object_reference] to be referred to by the
+     [full_user_name] (and its suffixes according to [visibility]).
+     [full_user_name] can either be a [full_path] or a [dir_path].
+   }
+   {- [exists : full_user_name -> bool]
+
+     Is the [full_user_name] already atributed as an absolute user name
+     of some object?
+   }
+   {- [locate : qualid -> object_reference]
+
+     Finds the object referred to by [qualid] or raises [Not_found]
+   }
+   {- [full_name : qualid -> full_user_name]
+
+     Finds the full user name referred to by [qualid] or raises [Not_found]
+   }
+   {- [shortest_qualid_of : object_reference -> user_name]
+
+     The [user_name] can be for example the shortest non ambiguous [qualid] or
+     the [full_user_name] or [identifier]. Such a function can also have a
+     local context argument.}}
 *)
 
 
@@ -70,14 +67,12 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a
 (** {6 Register visibility of things } *)
 
 (** The visibility can be registered either
-   {% \begin{%}itemize{% }%}
 
-   \item for all suffixes not shorter then a given int -- when the
-   object is loaded inside a module -- or
+   - for all suffixes not shorter then a given int -- when the
+     object is loaded inside a module -- or
 
-   \item for a precise suffix, when the module containing (the module
+   - for a precise suffix, when the module containing (the module
    containing ...) the object is opened (imported)
-   {% \end{%}itemize{% }%}
 *)
 
 type visibility = Until of int | Exactly of int
@@ -138,7 +133,7 @@ val full_name_cci : qualid -> full_path
 val full_name_modtype : qualid -> full_path
 val full_name_module : qualid -> dir_path
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Reverse lookup -- finding user names corresponding to the given
   internal name *)
 
diff --git a/library/states.mli b/library/states.mli
index f0dab29f2..9b5872bde 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -6,8 +6,9 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(** {6 Sect } *)
-(** States of the system. In that module, we provide functions to get
+(** {6 States of the system} *)
+
+(** In that module, we provide functions to get
   and set the state of the whole system. Internally, it is done by
   freezing the states of both [Lib] and [Summary]. We provide functions
   to write and restore state to and from a given file. *)
@@ -19,14 +20,13 @@ type state
 val freeze : unit -> state
 val unfreeze : state -> unit
 
-(** {6 Sect } *)
-(** Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the
+(** {6 Rollback } *)
+
+(** [with_heavy_rollback f x] applies [f] to [x] and restores the
   state of the whole system as it was before the evaluation if an exception
   is raised. *)
-
 val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
 
-(** {6 Sect } *)
 (** [with_state_protection f x] applies [f] to [x] and restores the
   state of the whole system as it was before the evaluation of f *)
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 890aa005c..6184ed7a1 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -82,7 +82,8 @@ val lookup_path_to_sort_from : env -> evar_map -> types ->
 val lookup_pattern_path_between :
   inductive * inductive -> (constructor * int) list
 
-(*i Crade *)
+(**/**)
+(* Crade *)
 open Pp
 val install_path_printer :
   ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 8ea91d28f..1ddf97c86 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -21,7 +21,8 @@ val the_conv_x_leq : env -> constr -> constr -> evar_map -> evar_map
 val e_conv  : env -> evar_map ref -> constr -> constr -> bool
 val e_cumul : env -> evar_map ref -> constr -> constr -> bool
 
-(*i For debugging *)
+(**/**)
+(* For debugging *)
 val evar_conv_x :
   env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
 val evar_eqappr_x :
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ebf91b4f4..43f214d0d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -162,7 +162,7 @@ val is_evar : evar_map -> evar -> bool
 
 val is_defined : evar_map -> evar -> bool
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
     no body and [Not_found] if it does not exist in [sigma] *)
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index eba26bafe..18a6b03a7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -81,8 +81,7 @@ sig
   val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
 
   (**/**)
-  (** Internal of Pretyping...
-   *)
+  (** Internal of Pretyping... *)
   val pretype :
     type_constraint -> env -> evar_map ref ->
     var_map * (identifier * identifier option) list ->
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 78b01eeab..5651b7687 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -13,7 +13,9 @@ open Libnames
 open Libobject
 open Library
 
-(** {6 Sect } *)
+(** Operations concerning records and canonical structures *)
+
+(** {6 Records } *)
 (** A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
@@ -51,7 +53,7 @@ val methods_matching : constr ->
   ((global_reference*Evd.evar*Evd.evar_map) *
      (constr*existential_key)*Termops.subst) list
 
-(** {6 Sect } *)
+(** {6 Canonical structures } *)
 (** A canonical structure declares "canonical" conversion hints between 
     the effective components of a structure and the projections of the  
     structure *)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9f3884088..5a0ba3cab 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -120,7 +120,7 @@ type meta_type_map = (metavariable * types) list
 (** [pop c] lifts by -1 the positive indexes in [c] *)
 val pop : constr -> constr
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** Substitution of an arbitrary large term. Uses equality modulo
    reduction of let *)
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 194dd1464..112003e8d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -23,7 +23,7 @@ open Tacexpr
    or [Theorem]), and ``goal'' means a subgoal of the current focused
    proof *)
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [refining ()] tells if there is some proof in progress, even if a not
    focused one *)
 
@@ -34,7 +34,7 @@ val refining : unit -> bool
 
 val check_no_pending_proofs : unit -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [delete_proof name] deletes proof of name [name] or fails if no proof
     has this name *)
 
@@ -49,7 +49,7 @@ val delete_current_proof : unit -> unit
 
 val delete_all_proofs : unit -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [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 *)
@@ -69,7 +69,7 @@ val current_proof_depth: unit -> int
 val set_undo : int option -> unit
 val get_undo : unit -> int option
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [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
@@ -89,7 +89,7 @@ val start_proof :
 
 val restart_proof : unit -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [resume_last_proof ()] focus on the last unfocused proof or fails
    if there is no suspended proofs *)
 
@@ -105,7 +105,7 @@ val resume_proof : identifier located -> unit
 
 val suspend_proof : unit -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [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;
@@ -119,7 +119,7 @@ val cook_proof : (Proof.proof -> unit) ->
 (** To export completed proofs to xml *)
 val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [get_Proof.proof ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
 
@@ -140,7 +140,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env
 val current_proof_statement :
   unit -> identifier * goal_kind * types * declaration_hook
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [get_current_proof_name ()] return the name of the current focused
     proof or failed if no proof is focused *)
 
@@ -150,13 +150,13 @@ val get_current_proof_name : unit -> identifier
 
 val get_all_proof_names : unit -> identifier list
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [set_end_tac tac] applies tactic [tac] to all subgoal generate
     by [solve_nth] *)
 
 val set_end_tac : tactic -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [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 *)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 8def61112..b07389cee 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -65,7 +65,7 @@ type prim_rule =
                                               in the type of evar] \} \} \} v}
 *)
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** 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
diff --git a/tactics/auto.mli b/tactics/auto.mli
index f7c3fd777..684478d96 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -20,6 +20,8 @@ open Libnames
 open Vernacexpr
 open Mod_subst
 
+(** Auto and related automation tactics *)
+
 type auto_tactic =
   | Res_pf     of constr * clausenv    (** Hint Apply *)
   | ERes_pf    of constr * clausenv    (** Hint EApply *)
@@ -122,11 +124,11 @@ val make_apply_entry :
       -> hint_entry
 
 (** A constr which is Hint'ed will be:
-   (1) used as an Exact, if it does not start with a product
-   (2) used as an Apply, if its HNF starts with a product, and
-       has no missing arguments.
-   (3) used as an EApply, if its HNF starts with a product, and
-       has missing arguments. *)
+   - (1) used as an Exact, if it does not start with a product
+   - (2) used as an Apply, if its HNF starts with a product, and
+         has no missing arguments.
+   - (3) used as an EApply, if its HNF starts with a product, and
+         has missing arguments. *)
 
 val make_resolves :
   env -> evar_map -> bool * bool * bool -> int option -> constr ->
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3fa8596f9..c44eb6fdd 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -14,7 +14,8 @@ open Evd
 open Pattern
 open Coqlib
 
-(** {6 Sect } *)
+(** High-order patterns *)
+
 (** Given a term with second-order variables in it,
    represented by Meta's, and possibly applied using SoApp
    terms, this function will perform second-order, binding-preserving,
@@ -34,7 +35,6 @@ open Coqlib
    intersection of the free-rels of the term and the current stack be
    contained in the arguments of the application *)
 
-(** {6 Sect } *)
 (** I implemented the following functions which test whether a term [t]
    is an inductive but non-recursive type, a general conjuction, a
    general disjunction, or a type with no constructors.
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index ed3a928ab..dae4e8e30 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -64,5 +64,5 @@ sig
   val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option
   val constr_val_discr : constr -> (term_label * constr list) lookup_res
     
-(**/**)
+  (**/**)
 end
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 446cdc1b3..ab8329fb0 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -19,18 +19,16 @@ open Redexpr
 open Constrintern
 open Pfedit
 
-(** {6 Sect } *)
 (** This file is about the interpretation of raw commands into typed
     ones and top-level declaration of the main Gallina objects *)
 
-(** Hooks for Pcoq *)
+(** {6 Hooks for Pcoq} *)
 
 val set_declare_definition_hook : (definition_entry -> unit) -> unit
 val get_declare_definition_hook : unit -> (definition_entry -> unit)
 val set_declare_assumptions_hook : (types -> unit) -> unit
 
-(************************************************************************
-   Definitions/Let *)
+(** {6 Definitions/Let} *)
 
 val interp_definition :
   boxed_flag -> local_binder list -> red_expr option -> constr_expr ->
@@ -39,8 +37,7 @@ val interp_definition :
 val declare_definition : identifier -> locality * definition_object_kind ->
   definition_entry -> manual_implicits -> declaration_hook -> unit
 
-(************************************************************************
-   Parameters/Assumptions *)
+(** {6 Parameters/Assumptions} *)
 
 val interp_assumption :
   local_binder list -> constr_expr -> types * manual_implicits
@@ -53,8 +50,7 @@ val declare_assumptions : variable located list ->
   coercion_flag -> assumption_kind -> types -> manual_implicits ->
   bool -> bool -> unit
 
-(************************************************************************
-   Inductive and coinductive types *)
+(** {6 Inductive and coinductive types} *)
 
 (** Extracting the semantical components out of the raw syntax of mutual
    inductive declarations *)
@@ -94,8 +90,7 @@ val declare_mutual_inductive_with_eliminations :
 val do_mutual_inductive :
   (one_inductive_expr * decl_notation list) list -> bool -> unit
 
-(************************************************************************
-   Fixpoints and cofixpoints *)
+(** {6 Fixpoints and cofixpoints} *)
 
 type structured_fixpoint_expr = {
   fix_name : identifier;
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index 55d7dcf2e..6bc449d5b 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -34,7 +34,7 @@ val start_proof_with_initialization :
 (** A hook the next three functions pass to cook_proof *)
 val set_save_hook : (Proof.proof -> unit) -> unit
 
-(** {6 Sect } *)
+(** {6 ... } *)
 (** [save_named b] saves the current completed proof under the name it
 was started; boolean [b] tells if the theorem is declared opaque; it
 fails if the proof is not completed *)