From: Andrea Asperti Date: Fri, 22 Dec 2006 10:37:35 +0000 (+0000) Subject: In the let-in case we compute the type and add it to the context. X-Git-Tag: 0.4.95@7852~711 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5682bf51adcde903c53a96e05475a7ded8fb255d;p=helm.git In the let-in case we compute the type and add it to the context. Before it was computed every time --- diff --git a/components/cic_acic/cic2acic.ml b/components/cic_acic/cic2acic.ml index 6cb2ad9a2..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 @@ -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