From: Claudio Sacerdoti Coen 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