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

4 files changed, 22 insertions, 35 deletions

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index bf28e0850a..880f8a4be2 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 a80e749d30..1d7f571b3a 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 224fb1d45b..3da9ec0e5a 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 2b95067473..8f1fa5c3d4 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