From 0e65684cf660f481b9fdf507c8c2b9b958c49596 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 14 Jan 2001 20:46:45 +0000 Subject: Petit bug encore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1250 85f007b7-540e-0410-9357-904b9bb8a0f7 --- lib/profile.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/profile.ml b/lib/profile.ml index ad47cebc4d..b95d9d02b7 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -84,7 +84,7 @@ let init_profile () = outside.tottime <- - !init_time; outside.owntime <- - !init_time -let ajoute o n = +let ajoute n o = o.owntime <- o.owntime + n.owntime; o.tottime <- o.tottime + n.tottime; o.hiownalloc <- o.hiownalloc + n.hiownalloc; @@ -96,7 +96,7 @@ let ajoute o n = o.immcount <- o.immcount + n.immcount let ajoute_to_list ((name,n) as e) l = - try ajoute (List.assoc name l) n; l + try ajoute n (List.assoc name l); l with Not_found -> e::l let magic = 1249 -- cgit v1.2.3