From eba0d24f94f4ab4744d3c9a0ddf4af267cd908ce Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 13 Jul 2017 20:35:10 +0200 Subject: [PATCH] Fixed bug in eta_subterm (cherry picked from commit 09ecd6ebdb7d96386bd79a7117930aba4635f778) --- ocaml/num.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 -- 2.39.2