X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralOptimizer.ml;h=6910613d29b3b2d2bf778b751e1ce0b268339277;hb=aefcb5f4e531c0318b7f495956c28eab971a4aa1;hp=a05bbd26d8df836d422b6fee82dd838b44840281;hpb=5b45f78ed4293ebbe8cc73ad925bca11a300d021;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml
index a05bbd26d..6910613d2 100644
--- a/helm/software/components/acic_procedural/proceduralOptimizer.ml
+++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml
@@ -253,6 +253,7 @@ let wrap g st c bo =
 
 let optimize_obj = function
    | C.Constant (name, Some bo, ty, pars, attrs) ->
+      let count_nodes = I.count_nodes ~meta:false 0 in 
       let st, c = {info = ""; dummy = ()}, [] in
       let bo, ty = H.cic_bc c bo, H.cic_bc c ty in 
       let g st bo =
@@ -262,14 +263,14 @@ let optimize_obj = function
 	    Ut.pp_term prerr_string [] c bo; prerr_newline ()
 	 end;
 (*	 let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *)
-         let nodes = Printf.sprintf "Optimized nodes: %u" (I.count_nodes 0 bo) in
+         let nodes = Printf.sprintf "Optimized nodes: %u" (count_nodes bo) in
 	 let st = info st nodes in
 	 L.time_stamp ("PO: DONE       " ^ name);
 	 C.Constant (name, Some bo, ty, pars, attrs), st.info
       in
       L.time_stamp ("PO: OPTIMIZING " ^ name);
       if !debug then Printf.eprintf "BEGIN: %s\n" name;
-      let nodes = Printf.sprintf "Initial nodes: %u" (I.count_nodes 0 bo) in
+      let nodes = Printf.sprintf "Initial nodes: %u" (count_nodes bo) in
       wrap g (info st nodes) c bo
    | obj                                         -> obj, ""