From 6b2d99445d35ea71cd24becb7f936e0cc9779d46 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 8 Feb 2001 08:29:12 +0000
Subject: simplification du make depend; fonctions de stat. util. memoire dans
 certains modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 8 +++++++-
 lib/util.mli | 4 +++-
 2 files changed, 10 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index e7cf325640..b5611c50b1 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -551,8 +551,14 @@ module Size = struct
     traverse (repr o);
     !count
 
-  let size_b o = (size_w o) * Sys.word_size lsr 3
+  let size_b o = (size_w o) * (Sys.word_size / 8)
+
+  let size_kb o = (size_w o) / (8192 / Sys.word_size)
 
 end
 
+let size_w = Size.size_w
 let size_b = Size.size_b
+let size_kb = Size.size_kb
+
+
diff --git a/lib/util.mli b/lib/util.mli
index fc3c980c6f..94d1d44f84 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -159,6 +159,8 @@ val prlist_with_sep :
 val prvect_with_sep :
    (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b array -> 'a Stream.t
 
-(*s Size of ocaml values. *)
+(*s Size of an ocaml value (in words, bytes and kilobytes). *)
 
+val size_w : 'a -> int
 val size_b : 'a -> int
+val size_kb : 'a -> int
-- 
cgit v1.2.3