in eta_finxing: type_of_aux' not called on eta_fixed terms

[helm.git] / helm / software / components / cic_acic / eta_fixing.ml

diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml
index 22d26e1bdd19920dc4906187efc992532bef0b8c..78789179f8c739e84c7c29abdaef003cc0f67731 100644 (file)
--- a/helm/software/components/cic_acic/eta_fixing.ml
+++ b/helm/software/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')