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=22d26e1bdd19920dc4906187efc992532bef0b8c;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml
index 22d26e1bd..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,20 +202,18 @@ 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)
-   | C.Appl l -> 
-       let l' =  List.map (eta_fix' context) l 
-       in 
-       (match l' with
-           [] -> assert false
-         | he::tl ->
-            let ty,_ = 
-              CicTypeChecker.type_of_aux' metasenv context he 
-		CicUniv.empty_ugraph 
-	    in
-              fix_according_to_type ty he tl
+        (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 
+       let ty,_ = 
+         CicTypeChecker.type_of_aux' metasenv context he 
+           CicUniv.empty_ugraph 
+       in
+       fix_according_to_type ty (eta_fix' context he) tl'
 (*
          C.Const(uri,exp_named_subst)::l'' ->
            let constant_type =
@@ -224,7 +225,7 @@ let eta_fix metasenv context t =
              ) in 
            fix_according_to_type 
              constant_type (C.Const(uri,exp_named_subst)) l''
-        | _ -> C.Appl l' *))
+        | _ -> C.Appl l' *)
    | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
         C.Const (uri,exp_named_subst')