diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-14 20:46:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-14 20:46:45 +0000 |
| commit | 0e65684cf660f481b9fdf507c8c2b9b958c49596 (patch) | |
| tree | 9a16e86d1b5372064d834a4e63807e6b5c60763e /lib | |
| parent | 9907ff67a01b9cc0426270332f14b1e2822b64ab (diff) | |
Petit bug encore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1250 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/profile.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/profile.ml b/lib/profile.ml index ad47cebc4..b95d9d02b 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 |