matitaprover

[helm.git] / helm / software / components / cic_acic / cic2acic.ml

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index e1c964c76073ac21388a1abf79ee9968c0c45e23..6da6484535f53f3922ad0f735074727c02c32a3e 100644 (file)
--- 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 =
@@ -477,7 +474,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
       ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
-let acic_object_of_cic_object ?(eta_fix=true) obj =
+let acic_object_of_cic_object ?(eta_fix=false) obj =
  let module C = Cic in
  let module E = Eta_fixing in
   let ids_to_terms = Hashtbl.create 503 in