prvecti

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

2 files changed, 14 insertions, 2 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 77d26ecf4..59f119a50 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -390,6 +390,16 @@ let rec prlist_with_sep sep elem l = match l with
       let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
       [< e; s; r >]
       
+let prvecti elem v =
+  let n = Array.length v in
+  let rec pr i =
+    if i = 0 then 
+      elem 0 v.(0)
+    else
+      let r = pr (i-1) and e = elem i v.(i) in [< r; e >]
+  in
+  pr (n-1)
+
 let prvect_with_sep sep elem v =
   let rec pr n =
     if n = 0 then 
@@ -397,5 +407,6 @@ let prvect_with_sep sep elem v =
     else 
       let r = pr (n-1) and s = sep() and e = elem v.(n) in 
       [< r; s; e >]
-  in
-  if Array.length v = 0 then [< >] else pr (Array.length v - 1)
+      in
+  let n = Array.length v in
+  if n = 0 then [< >] else pr (n - 1)
diff --git a/lib/util.mli b/lib/util.mli
index 30d7bdee7..b8b72da09 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -123,6 +123,7 @@ val pr_str : string -> std_ppcmds
 val pr_coma : unit -> std_ppcmds
 
 val prlist : ('a -> 'b Stream.t) -> 'a list -> 'b Stream.t
+val prvecti : (int -> 'a -> 'b Stream.t) -> 'a array -> 'b Stream.t
 val prlist_with_sep :
    (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b list -> 'a Stream.t
 val prvect_with_sep :