module Refiner

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@109 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 440acd6ba2..0f900ff923 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -127,6 +127,25 @@ let list_except x l = List.filter (fun y -> not (x = y)) l
 
 let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
 
+let list_map_i f = 
+  let rec map_i_rec i = function
+    | [] -> [] 
+    | x::l -> let v = f i x in v::map_i_rec (i+1) l
+  in 
+  map_i_rec
+
+let rec list_sep_last = function
+  | [] -> failwith "sep_last"
+  | hd::[] -> (hd,[])
+  | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
+
+let list_try_find_i f = 
+  let rec try_find_f n = function
+    | [] -> failwith "try_find_i"
+    | h::t -> try f n h with Failure _ -> try_find_f (n+1) t
+  in 
+  try_find_f
+
 (* Arrays *)
 
 let array_exists f v =