Fixes previous wrong commit.

[helm.git] / matita / matita / matitaEngine.ml

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 2d0a03b20da91e058f0f522cc7e0ad8fcadf1e65..5d16763fc36ad6db0b685937e47e53fdc11e2c5b 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -292,7 +292,7 @@ and compile ~compiling ~asserted ~include_paths fname =
       if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
       else pp_ast_statement
     in
-    let asserted, times, status =
+    let asserted, status =
      eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin