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

13 files changed, 59 insertions, 41 deletions

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