From: Claudio Sacerdoti Coen Date: Thu, 30 Mar 2006 16:21:45 +0000 (+0000) Subject: Profiling code for merge_ugraphs commented out (since profiling is much more X-Git-Tag: 0.4.95@7852~1539 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=72f4c53c7d74a971ae89a9c2ae42d9265f39fcd4;p=helm.git Profiling code for merge_ugraphs commented out (since profiling is much more expensive than the profiled code). --- diff --git a/components/cic/cicUniv.ml b/components/cic/cicUniv.ml index 8ae118c9b..b77830954 100644 --- a/components/cic/cicUniv.ml +++ b/components/cic/cicUniv.ml @@ -600,10 +600,13 @@ let merge_ugraphs ~base_ugraph ~increment:(increment, uri_of_increment) = fst (merge_brutal increment base_ugraph), UriManager.UriSet.add uri_of_increment already_contained -let profiler_merge = HExtlib.profile "CicUniv.merge_graphs" +(* profiling code; WARNING: the time spent during profiling can be + greater than the profiled time +let profiler_merge = HExtlib.profile "CicUniv.merge_ugraphs" let merge_ugraphs ~base_ugraph ~increment = profiler_merge.HExtlib.profile (fun _ -> merge_ugraphs ~base_ugraph ~increment) () +*) (*****************************************************************************) (** Xml sesialization and parsing **)