From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jul 2012 22:58:14 +0000 (+0000)
Subject: Some debugging times exposed.
X-Git-Tag: make_still_working~1602
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=789be8e12d78acc622fc9a115c592fa42b8fa3d1;p=helm.git

Some debugging times exposed.
---

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 57491cbda..a4942aa07 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -915,8 +915,13 @@ let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
        let status =
         List.fold_left 
           (fun status tac ->
+            let time0 = Unix.gettimeofday () in
             let status = eval_ng_tac (text,prefix_len,tac) status in
-            subst_metasenv_and_fix_names status)
+            let time3 = Unix.gettimeofday () in
+            HLog.debug ("... eval_ng_tac done in " ^ string_of_float (time3 -. time0) ^ "s");
+            let status = subst_metasenv_and_fix_names status in
+            let time3 = Unix.gettimeofday () in
+            HLog.debug ("... subst_metasenv_and_fix_names done in " ^ string_of_float (time3 -. time0) ^ "s"); status)
           status tacl
        in
         status