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

6 files changed, 11 insertions, 8 deletions

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 *)