From 513b547b55c73b2579206d762f0a136c3b11a66b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Oct 2000 13:35:40 +0000
Subject: Bug dans [prvecti v] quand v est vide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@681 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index c733ed3335..dd5be58714 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -480,7 +480,7 @@ let prvecti elem v =
     else
       let r = pr (i-1) and e = elem i v.(i) in [< r; e >]
   in
-  pr (n-1)
+  if n=0 then [< >] else pr (n - 1)
 
 let prvect_with_sep sep elem v =
   let rec pr n =
-- 
cgit v1.2.3