From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 1 Jun 2007 19:32:06 +0000 (+0000)
Subject: Profiling enabled again.
X-Git-Tag: 0.4.95@7852~410
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5fa1028bbaa9092cd86133b923f83945fba6b10;p=helm.git

Profiling enabled again.
---

diff --git a/matita/contribs/formal_topology/bin/theory_explorer.ml b/matita/contribs/formal_topology/bin/theory_explorer.ml
index 69911cfb3..da4bd3cde 100644
--- a/matita/contribs/formal_topology/bin/theory_explorer.ml
+++ b/matita/contribs/formal_topology/bin/theory_explorer.ml
@@ -7,7 +7,7 @@ let profile f x =
  let res = f x in
  let after = Unix.gettimeofday () in
  let delta = after -. before in
-  if res = Unix.WEXITED 0 then
+  if res then
    ok_time := !ok_time +. delta
   else
    ko_time := !ko_time +. delta;
@@ -256,7 +256,7 @@ let test to_be_considered_and_now ((s,_,_) as set) rel candidate repr =
   output_string ch (query ^ "\n");
   close_out ch;
 *)
-  let res = exec_cmds [query1; query2; query3; query4] in
+  let res = profile exec_cmds [query1; query2; query3; query4] in
 (*
   let res =
    (*Unix.system "../../../matitac.opt xxx.ma >> log 2>&1" = Unix.WEXITED 0*)