Some debugging times exposed.

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index 57491cbdaf4d4ddf46f936b415f1622d100f6d72..a4942aa07f690017643a88e21ba859a6c77107cf 100644 (file)
--- 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