removed deadcode / fixed typos (thanks to ocaml 3.09)

[helm.git] / helm / ocaml / cic_acic / eta_fixing.ml

diff --git a/helm/ocaml/cic_acic/eta_fixing.ml b/helm/ocaml/cic_acic/eta_fixing.ml
index 68dec37d6b04230f1468665e0a6f77516ccdb365..75e66d93484bed59b5e0f09fb0d29c788a90ffe9 100644 (file)
--- 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 =