nouvel algo de conversion plus uniforme

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

2 files changed, 12 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 7435504816..30e64307d1 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -342,6 +342,16 @@ let array_fold_left_i f v a =
   let rec fold i v = if i = n then v else fold (succ i) (f i v a.(i)) in
   fold 0 v
 
+let array_fold_right2 f v1 v2 a =
+  let lv1 = Array.length v1 in
+  let rec fold a n =
+    if n=0 then a
+    else
+      let k = n-1 in
+      fold (f v1.(k) v2.(k) a) k in
+  if Array.length v2 <> lv1 then invalid_arg "array_fold_right2";
+  fold a lv1
+
 let array_fold_left2 f a v1 v2 =
   let lv1 = Array.length v1 in
   let rec fold a n = 
diff --git a/lib/util.mli b/lib/util.mli
index bbf5cf240f..7bd7d71c46 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -107,6 +107,8 @@ val array_cons : 'a -> 'a array -> 'a array
 val array_fold_right_i : 
   (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
 val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
+val array_fold_right2 :
+  ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
 val array_fold_left2 : 
   ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
 val array_fold_left2_i :