Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / ocaml / cic / cicUtil.ml

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index bb356655a663477e79ff55333fd1c4d594191832..1af68ce39d4995a20c95f41ed5f013c3cbbe841c 100644 (file)
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -115,24 +115,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(\\(.*\\))"