X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=72837dab0f954b3e264284a480d833357c13f186;hb=e8f64678cc425f19336ff4f905f9b2f00acd6627;hp=e1c964c76073ac21388a1abf79ee9968c0c45e23;hpb=6a4cf39f4ad37545b33db31f3610d960375ce2a5;p=helm.git

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index e1c964c76..72837dab0 100644
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -135,7 +135,6 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
    prerr_endline
     ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
 *)
-    let time = ref 0. in
     let rec aux computeinnertypes father context idrefs tt =
      let fresh_id'' = fresh_id' father tt in
      (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
@@ -386,9 +385,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
            ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
           res
 *)
-  let res = aux global_computeinnertypes None context idrefs t in
-  prerr_endline (">>>> aux : " ^ string_of_float !time);
-  res
+  aux global_computeinnertypes None context idrefs t
 ;;
 
 let acic_of_cic_context ~computeinnertypes metasenv context idrefs t =