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