time stamps dans System

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@54 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 23 insertions, 17 deletions

diff --git a/lib/system.ml b/lib/system.ml
new file mode 100644
index 000000000..fe0efa073
--- /dev/null
+++ b/lib/system.ml
@@ -0,0 +1,13 @@
+
+(* $Id$ *)
+
+(* Time stamps. *)
+
+type time_stamp = float
+
+let get_time_stamp () = Unix.time()
+
+let compare_time_stamps t1 t2 =
+  let dt = t2 -. t1 in
+  if dt < 0.0 then -1 else if dt = 0.0 then 0 else 1
+
diff --git a/lib/system.mli b/lib/system.mli
new file mode 100644
index 000000000..13265d1d8
--- /dev/null
+++ b/lib/system.mli
@@ -0,0 +1,10 @@
+
+(* $Id$ *)
+
+(*s Time stamps. *)
+
+type time_stamp
+
+val get_time_stamp : unit -> time_stamp
+val compare_time_stamps : time_stamp -> time_stamp -> int
+
diff --git a/lib/util.ml b/lib/util.ml
index deb810cdd..34ad89aa2 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -263,16 +263,6 @@ let option_app f = function
   | None -> None
   | Some x -> Some (f x)
 
-(* Time stamps. *)
-
-type time_stamp = float
-
-let get_time_stamp () = Unix.time()
-
-let compare_time_stamps t1 t2 =
-  let dt = t2 -. t1 in
-  if dt < 0.0 then -1 else if dt = 0.0 then 0 else 1
-
 (* Pretty-printing *)
   
 let pr_spc () = [< 'sPC >];;
diff --git a/lib/util.mli b/lib/util.mli
index 0ef34a841..c8f3eb6db 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -74,13 +74,6 @@ module Intset : Set.S with type elt = int
 
 val option_app : ('a -> 'b) -> 'a option -> 'b option
 
-(*s Time stamps. *)
-
-type time_stamp
-
-val get_time_stamp : unit -> time_stamp
-val compare_time_stamps : time_stamp -> time_stamp -> int
-
 (*s Pretty-printing. *)
 
 val pr_spc : unit -> std_ppcmds