X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=3ac5670956e91e3c4407985007b3a519b118d386;hb=2fb7dd29bac6ee7add3618c5d798fa60ab0c8eb4;hp=c5958575afe939125ea650cd58286229147ddbd0;hpb=2ea5357bace160aaf57750d9dcfb3077fe5a1b38;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index c5958575a..3ac567095 100644
--- 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);