Add list_iter3

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

2 files changed, 9 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 32ede2fb2..5e3f7fa6b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -262,6 +262,14 @@ let rec list_fold_right_and_left f l hd =
     | a::l -> let hd = aux (a::tl) l in f hd a tl
    in aux [] l
 
+let list_iter3 f l1 l2 l3 =
+  let rec iter = function
+    | ([], [], []) -> ()
+    | ((h1::t1), (h2::t2), (h3::t3)) -> f h1 h2 h3; iter (t1,t2,t3)
+    | (_, _, _) -> invalid_arg "map3"
+  in 
+  iter (l1,l2,l3)
+
 let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
 
 let list_for_all_i p = 
diff --git a/lib/util.mli b/lib/util.mli
index 8e3ec2cb4..ae1b906ce 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -111,6 +111,7 @@ val list_index : 'a -> 'a list -> int
 val list_unique_index : 'a -> 'a list -> int 
 (* [list_index0] behaves as [list_index] except that it starts counting at 0 *)
 val list_index0 : 'a -> 'a list -> int
+val list_iter3 : ('a -> 'b -> 'c -> unit) -> 'a list -> 'b list -> 'c list -> unit
 val list_iter_i :  (int -> 'a -> unit) -> 'a list -> unit
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_fold_right_and_left :