aboutsummaryrefslogtreecommitdiff
path: root/lib/util.ml
diff options
context:
space:
mode:
authorherbelin2012-03-20 08:02:11 +0000
committerherbelin2012-03-20 08:02:11 +0000
commit541ff113562c62381100caea84bf58ce5b2cd3ce (patch)
tree5e194ce12f2a98843bb0a39818715838e1905bd7 /lib/util.ml
parent0a59c2e537040d3e74fd65cd738fa617cbd4f1e2 (diff)
Reorganizing the structure of evarutil.ml (only restructuration, no
change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml12
1 files changed, 12 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml
index e6c76f7f3d..2bbdc76cf9 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -666,6 +666,12 @@ let list_map_filter_i f =
match f i x with None -> l' | Some y -> y::l'
in aux 0
+let list_filter_along f filter l =
+ snd (list_filter2 (fun b c -> f b) (filter,l))
+
+let list_filter_with filter l =
+ list_filter_along (fun x -> x) filter l
+
let list_subset l1 l2 =
let t2 = Hashtbl.create 151 in
List.iter (fun x -> Hashtbl.add t2 x ()) l2;
@@ -1183,6 +1189,12 @@ let array_rev_to_list a =
if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in
tolist 0 []
+let array_filter_along f filter v =
+ Array.of_list (list_filter_along f filter (Array.to_list v))
+
+let array_filter_with filter v =
+ Array.of_list (list_filter_with filter (Array.to_list v))
+
(* Stream *)
let stream_nth n st =