Changement de la structure des points fixes

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

2 files changed, 10 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 44b5ef08fa..cd32737d2e 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -322,6 +322,14 @@ let array_last v =
 
 let array_cons e v = Array.append [|e|] v
 
+let array_fold_right_i f v a =
+  let rec fold a n =
+    if n=0 then a
+    else
+      let k = n-1 in
+      fold (f k v.(k) a) k in
+  fold a (Array.length v)
+
 let array_fold_left_i f v a =
   let n = Array.length a in
   let rec fold i v = if i = n then v else fold (succ i) (f i v a.(i)) in
diff --git a/lib/util.mli b/lib/util.mli
index 8938257898..5122df3e89 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -103,6 +103,8 @@ val array_hd : 'a array -> 'a
 val array_tl : 'a array -> 'a array
 val array_last : 'a array -> 'a
 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_left2 : 
   ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a