X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_acic%2Feta_fixing.ml;h=22d26e1bdd19920dc4906187efc992532bef0b8c;hb=f1dc70ca55058b2983cd23b829d856df3b41b9a7;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..22d26e1bd 100644
--- a/helm/ocaml/cic_acic/eta_fixing.ml
+++ b/helm/ocaml/cic_acic/eta_fixing.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 exception ReferenceToNonVariable;;
 
 let prerr_endline _ = ();;
@@ -200,7 +202,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 +234,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 +276,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 =