librarian: improved error detection, bug fix in time comparison functions: now the...

[helm.git] / helm / software / components / acic_procedural / proceduralOptimizer.ml

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index c5958575afe939125ea650cd58286229147ddbd0..3ac5670956e91e3c4407985007b3a519b118d386 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -34,6 +34,7 @@ module HEL  = HExtlib
 module PEH  = ProofEngineHelpers
 module TC   = CicTypeChecker 
 module Un   = CicUniv
+module L    = Librarian
 
 module H    = ProceduralHelpers
 module Cl   = ProceduralClassify
@@ -285,11 +286,11 @@ let optimize_obj = function
            prerr_string "H.pp_term : ";
            H.pp_term prerr_string [] [] bo; prerr_newline ()
         end;
-        let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in
-        H.print_times ("OPTIMIZED: " ^ name);
+(*      let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *)
+        L.time_stamp ("PO: DONE       " ^ name);
         C.Constant (name, Some bo, ty, pars, attrs)
       in
-      H.print_times ("BEGIN    : " ^ name);
+         L.time_stamp ("PO: OPTIMIZING " ^ name);
       if !debug then
          Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" 
             name (I.count_nodes 0 bo);