diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-23 15:04:09 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-23 15:04:09 +0000 |
| commit | fae106f740d3d71555933cf416eec905c58f417e (patch) | |
| tree | 12cfd6fa08b20e9f076c113a1a668388c5cf5527 /lib | |
| parent | fab1cc89b9ff65938cff3b4e41e51ad3b0bc68db (diff) | |
amelioration de la consommation memoire de la conversion en eta-expansant
les definitions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/profile.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/profile.ml b/lib/profile.ml index 825b792d7..f02e6fa5a 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -26,9 +26,9 @@ let get_alloc () = Gc.allocated_bytes () let get_alloc_overhead = let now = get_alloc () in let after = get_alloc () in - after -. now (* Rem: overhead is 16 bytes in ocaml 3.00 *) + after -. now (* Rem: overhead is 16 bytes in ocaml 3.00 *) -let last_alloc = ref 0.0 +let last_alloc = ref (get_alloc()) (* spent_alloc returns a integer in Z/31Z (or Z/63Z) *) (* remark: it cannot detect allocations steps more than 2^31 (or 2^63) *) @@ -122,7 +122,7 @@ let ajoute_to_list ((name,n) as e) l = with Not_found -> e::l let magic = 1249 - + let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = let (old_table, old_outside, old_total) = try |