diff options
| author | letouzey | 2010-04-29 16:06:42 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-29 16:06:42 +0000 |
| commit | ccba6c718af6a5a15f278fc9365b6ad27108e98f (patch) | |
| tree | f0229aa4d08eb12db1fb1e76f227076c117d59bf /lib | |
| parent | 06456c76b7fa2f0c69380faf27a6ca403b1e6f3f (diff) | |
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
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/explore.mli | 4 | ||||
| -rw-r--r-- | lib/pp.mli | 2 | ||||
| -rw-r--r-- | lib/system.mli | 12 | ||||
| -rw-r--r-- | lib/util.mli | 4 |
4 files changed, 12 insertions, 10 deletions
diff --git a/lib/explore.mli b/lib/explore.mli index 0e8eb32bef..1f17f8a4c7 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 56e66225cb..ca62f82d6e 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 09142f3652..d8a4088d06 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 fd8ff9275f..f7f40b8056 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) *) |
