X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Feta_fixing.ml;h=90f33d0811bf39d8d8e462b21fe0bba50a715a5d;hb=ba5c1c83e77e701ef11625687ec27931bc4bb944;hp=78789179f8c739e84c7c29abdaef003cc0f67731;hpb=df0bf216c6bbebf452c1b107a5d995bd8dd16451;p=helm.git

diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml
index 78789179f..90f33d081 100644
--- a/helm/software/components/cic_acic/eta_fixing.ml
+++ b/helm/software/components/cic_acic/eta_fixing.ml
@@ -84,7 +84,8 @@ let rec fix_lambdas_wrt_type ty te =
       let t2 = 
          match t' with
            C.Appl l -> 
-             C.LetIn (C.Name "w",t',C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
+             C.LetIn (C.Name "w",t',assert false,
+              C.Appl ((C.Rel 1)::(mk_rels no_sources 1)))
          | _ -> C.Appl (t'::(mk_rels no_sources 0)) in
       List.fold_right
         (fun source t -> C.Lambda (C.Name "y",CicReduction.whd [] source,t)) sources t2
@@ -145,7 +146,9 @@ let fix_according_to_type ty hd tl =
               (* prerr_endline ("******* too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); *)
               C.LetIn 
                 (C.Name "H", 
-                  C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
+                  C.Appl res,
+                   assert false,
+                    C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
     else 
       let name,source,target =
         (match ty with
@@ -199,9 +202,10 @@ let eta_fix metasenv context t =
    | C.Lambda (n,s,t) -> 
        C.Lambda 
         (n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
-   | C.LetIn (n,s,t) -> 
+   | C.LetIn (n,s,ty,t) -> 
        C.LetIn 
-        (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
+        (n,eta_fix' context s,eta_fix' context ty,
+          eta_fix' ((Some (n,(C.Def (s,ty))))::context) t)
    | C.Appl [] -> assert false 
    | C.Appl (he::tl) -> 
        let tl' =  List.map (eta_fix' context) tl in