X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=a4942aa07f690017643a88e21ba859a6c77107cf;hb=faa43ddbbecba42c32653008d605f7c260c67a87;hp=57491cbdaf4d4ddf46f936b415f1622d100f6d72;hpb=46990564407e2402686022884767fc749a97d734;p=helm.git

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