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? *)
("+++++++++++++ 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 =
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
let aobj =
match obj with
C.Constant (id,Some bo,ty,params,attrs) ->
- let bo' = eta_fix [] [] bo in
+ let bo' = (*eta_fix [] []*) bo in
let ty' = eta_fix [] [] ty in
let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
(cid,i,acanonical_context,aterm))
conjectures' in
(* let time1 = Sys.time () in *)
- let bo' = eta_fix conjectures' [] bo in
+ let bo' = (*eta_fix conjectures' []*) bo in
let ty' = eta_fix conjectures' [] ty in
(*
let time2 = Sys.time () in