X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic%2FcicUtil.ml;h=7c6e3eabe28619cc14fdd0cb812f998566d38b52;hb=ed308fc03be5397081ac0e00bbc73b3f71da1e67;hp=bb356655a663477e79ff55333fd1c4d594191832;hpb=024819eeb7fcd370114ceb3dffc7907db92ab640;p=helm.git diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index bb356655a..7c6e3eabe 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf exception Meta_not_found of int @@ -115,24 +117,25 @@ let rec is_meta_closed = | Cic.Lambda (_,so,dest) -> is_meta_closed so && is_meta_closed dest | Cic.LetIn (_,so,dest) -> is_meta_closed so && is_meta_closed dest | Cic.Appl l -> - List.fold_right (fun x i -> i && is_meta_closed x) l true + not (List.exists (fun x -> not (is_meta_closed x)) l) | Cic.Var (_,exp_named_subst) | Cic.Const (_,exp_named_subst) | Cic.MutInd (_,_,exp_named_subst) | Cic.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && is_meta_closed x) - exp_named_subst true + not (List.exists (fun (_,x) -> not (is_meta_closed x)) exp_named_subst) | Cic.MutCase (_,_,out,te,pl) -> is_meta_closed out && is_meta_closed te && - List.fold_right (fun x i -> i && is_meta_closed x) pl true + not (List.exists (fun x -> not (is_meta_closed x)) pl) | Cic.Fix (_,fl) -> - List.fold_right - (fun (_,_,ty,bo) i -> i && is_meta_closed ty && is_meta_closed bo - ) fl true + not (List.exists + (fun (_,_,ty,bo) -> + not (is_meta_closed ty) || not (is_meta_closed bo)) + fl) | Cic.CoFix (_,fl) -> - List.fold_right - (fun (_,ty,bo) i -> i && is_meta_closed ty && is_meta_closed bo - ) fl true + not (List.exists + (fun (_,ty,bo) -> + not (is_meta_closed ty) || not (is_meta_closed bo)) + fl) ;; let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))"