X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_acic%2Feta_fixing.ml;h=75e66d93484bed59b5e0f09fb0d29c788a90ffe9;hb=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;hp=68dec37d6b04230f1468665e0a6f77516ccdb365;hpb=9a0e4f3be9f70662f18d2d3b6dd60ae79fba565b;p=helm.git

diff --git a/helm/ocaml/cic_acic/eta_fixing.ml b/helm/ocaml/cic_acic/eta_fixing.ml
index 68dec37d6..75e66d934 100644
--- a/helm/ocaml/cic_acic/eta_fixing.ml
+++ b/helm/ocaml/cic_acic/eta_fixing.ml
@@ -200,7 +200,7 @@ 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 as appl -> 
+   | C.Appl l -> 
        let l' =  List.map (eta_fix' context) l 
        in 
        (match l' with
@@ -232,7 +232,7 @@ let eta_fix metasenv context t =
    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
        let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
         C.MutConstruct (uri, tyno, consno, exp_named_subst')
-   | C.MutCase (uri, tyno, outty, term, patterns) as prima ->
+   | C.MutCase (uri, tyno, outty, term, patterns) ->
        let outty' =  eta_fix' context outty in
        let term' = eta_fix' context term in
        let patterns' = List.map (eta_fix' context) patterns in
@@ -274,7 +274,7 @@ let eta_fix metasenv context t =
              | _ -> prerr_endline ("QUA"); assert false) in 
        let patterns2 = 
          List.map2 fix_lambdas_wrt_type
-           constructor_types patterns in 
+           constructor_types patterns' in 
          C.MutCase (uri, tyno, outty',term',patterns2)
    | C.Fix (funno, funs) ->
        let fun_types =