X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2Fcic2acic.ml;h=6cb2ad9a21fbbf4afaa16c3704c97a979daecf47;hb=9ab7d3460c70ee067f75bf6523d06b67d6e7750a;hp=72837dab0f954b3e264284a480d833357c13f186;hpb=33b1f57feafa53d0520035f3a27f6c18c36f478d;p=helm.git

diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml
index 72837dab0..6cb2ad9a2 100644
--- a/components/cic_acic/cic2acic.ml
+++ b/components/cic_acic/cic2acic.ml
@@ -474,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
@@ -499,7 +499,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
    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
@@ -557,7 +557,7 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
            (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