X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_acic%2Feta_fixing.ml;h=78789179f8c739e84c7c29abdaef003cc0f67731;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=22d26e1bdd19920dc4906187efc992532bef0b8c;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_acic/eta_fixing.ml b/components/cic_acic/eta_fixing.ml
index 22d26e1bd..78789179f 100644
--- a/components/cic_acic/eta_fixing.ml
+++ b/components/cic_acic/eta_fixing.ml
@@ -202,17 +202,14 @@ let eta_fix metasenv context t =
    | C.LetIn (n,s,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
+   | 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 +221,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')