diff options
| author | filliatr | 1999-12-03 11:34:33 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-03 11:34:33 +0000 |
| commit | 76b16e44285d06236b9c00e24659138c376d54f3 (patch) | |
| tree | 03bb85046c204828901f26d84e2196c37abaa7f2 /lib/system.mli | |
| parent | f20dbafa3e49c35414640e01c3549ad1c802d331 (diff) | |
modules profile, Coqinit et Coqtop (=main)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@194 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/lib/system.mli b/lib/system.mli index 0c4bbd2284..e3fd5978c3 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -8,9 +8,12 @@ val is_in_path : string list -> string -> bool val where_in_path : string list -> string -> string val make_suffix : string -> string -> string +val file_readable_p : string -> bool val glob : string -> string +val home : string + (*s Global load path. *) val add_path : string -> unit @@ -34,8 +37,11 @@ val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a) (*s Time stamps. *) -type time_stamp +type time + +val process_time : unit -> float * float +val get_time : unit -> time +val time_difference : time -> time -> float (* in seconds *) +val fmt_time_difference : time -> time -> Pp.std_ppcmds -val get_time_stamp : unit -> time_stamp -val compare_time_stamps : time_stamp -> time_stamp -> int |