From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 26 May 2006 10:10:39 +0000 (+0000)
Subject: Profiling code removed.
X-Git-Tag: make_still_working~7325
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1cb502bc3e0c797bf9b4c92c75a849f44df687eb;p=helm.git

Profiling code removed.
---

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 =