X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fnum.ml;h=c88fa8de1a666cd68cbb8d1e5c10286fd38157f5;hb=87e0182247e9176ec3612eaf3c7f90b81f43b6f5;hp=95501a4e14cb0878e83196dde9dd4a438cd03683;hpb=16c320315ed4d5d0c4f67cffd36f028029c01a60;p=fireball-separation.git

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 95501a4..c88fa8d 100644
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -297,10 +297,10 @@ let rec eta_subterm sub t =
   | `Match(u,ar,liftno,bs,args) ->
      eta_subterm sub (u :> nf)
      || List.exists (fun (_, t) -> eta_subterm sub (lift liftno t)) !bs
-     || List.exists (eta_subterm sub) args
-  | `I(v, args) -> List.exists (eta_subterm sub) (Listx.to_list args) || (match sub with
-   | `Var v' -> v = v'
-   | `I(v', args') -> v = v'
+     || List.exists (eta_subterm sub) (args :> nf list)
+  | `I((v,_), args) -> List.exists (eta_subterm sub) ((Listx.to_list args) :> nf list) || (match sub with
+   | `Var(v',_) -> v = v'
+   | `I((v',_), args') -> v = v'
     && Listx.length args' < Listx.length args
     && List.for_all (fun (x,y) -> eta_eq x y) (List.combine (Util.take (Listx.length args') (Listx.to_list args)) (Listx.to_list args'))
    | _ -> false