X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_acic%2Fcic2acic.ml;h=d8392f6206ab745e2647a75286e30745e481e18a;hb=5682bf51adcde903c53a96e05475a7ded8fb255d;hp=6da6484535f53f3922ad0f735074727c02c32a3e;hpb=df8f668d1369432dbfb7c74a4c4789f3353fcb45;p=helm.git

diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml
index 6da648453..d8392f620 100644
--- a/components/cic_acic/cic2acic.ml
+++ b/components/cic_acic/cic2acic.ml
@@ -301,12 +301,19 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
                (fresh_id'',n, aux' context idrefs s,
                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
           | C.LetIn (n,s,t) ->
-             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = `Prop then
-              add_inner_type fresh_id'' ;
-             C.ALetIn
-              (fresh_id'', n, aux' context idrefs s,
-               aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
+             let s_ty =
+              try
+               (cic_CicHash_find terms_to_types s).D.synthesized
+              with
+               Not_found ->
+                cicReduction_whd context (xxx_type_of_aux' metasenv context s);
+             in
+              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
+              if innersort = `Prop then
+               add_inner_type fresh_id'' ;
+              C.ALetIn
+               (fresh_id'', n, aux' context idrefs s,
+                aux' ((Some (n, C.Def(s,Some s_ty)))::context) (fresh_id''::idrefs) t)
           | C.Appl l ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = `Prop then
@@ -499,7 +506,7 @@ let acic_object_of_cic_object ?(eta_fix=false) 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
@@ -556,8 +563,8 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
              = aconjecture_of_conjecture' conjectures conjecture 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 bo' = bo in
        let ty' = eta_fix conjectures' [] ty in
 (*
        let time2 = Sys.time () in