From ce014bf1c0912a7a48025e6184a27bd929089252 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 10 Aug 2011 14:27:41 +0000
Subject: Added list_map_filter_i

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14397 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 8 ++++++++
 lib/util.mli | 1 +
 2 files changed, 9 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index e9f87acb53..688d415840 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -695,6 +695,14 @@ let rec list_map_filter f = function
       let l' = list_map_filter f l in
       match f x with None -> l' | Some y -> y::l'
 
+let list_map_filter_i f =
+  let rec aux i = function
+    | [] -> []
+    | x::l ->
+      let l' = aux (succ i) l in
+	match f i x with None -> l' | Some y -> y::l'
+  in aux 0
+
 let list_subset l1 l2 =
   let t2 = Hashtbl.create 151 in
   List.iter (fun x -> Hashtbl.add t2 x ()) l2;
diff --git a/lib/util.mli b/lib/util.mli
index 7b8f9d31d7..e24df1a315 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -133,6 +133,7 @@ val list_distinct : 'a list -> bool
 val list_duplicates : 'a list -> 'a list
 val list_filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
 val list_map_filter : ('a -> 'b option) -> 'a list -> 'b list
+val list_map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
 
 (** [list_smartmap f [a1...an] = List.map f [a1...an]] but if for all i
    [ f ai == ai], then [list_smartmap f l==l] *)
-- 
cgit v1.2.3