X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple.ml;h=079774e5ac67e5c53feaa53eca9e7e622dd77c76;hb=b0ecd3e4062bb9012ea9623237d0b379bd7646f2;hp=60b4e8779f4aa41705dd8016fd3c2918599a74da;hpb=1f8f8e52c38e1897e9b5ea106721d6a4dd88c284;p=fireball-separation.git diff --git a/ocaml/simple.ml b/ocaml/simple.ml index 60b4e87..079774e 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -257,9 +257,11 @@ let inert_cut_at n t = let find_eta_difference p t = let divargs = args_of_inert p.div in let conargs = args_of_inert t in + let rec range i j = + if j = -1 then [] else i :: range (i+1) (j-1) in let rec aux k divargs conargs = match divargs,conargs with - [],_ -> [] + [],conargs -> range k (List.length conargs) | _::_,[] -> [k] | t1::divargs,t2::conargs -> (if not (eta_eq t1 t2) then [k] else []) @ aux (k+1) divargs conargs