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

10 files changed, 63 insertions, 70 deletions

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