For the beauty of tail recursion, a new list_addn

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

1 files changed, 9 insertions, 7 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 5cd351237..76d9c6728 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -428,10 +428,15 @@ let list_tabulate f len =
   in
   tabrec 0
 
-let rec list_make n v =
-  if n = 0 then []
-  else if n < 0 then invalid_arg "list_make"
-  else v::list_make (n-1) v
+let list_addn n v =
+  let rec aux n l =
+    if n = 0 then l
+    else aux (pred n) (v::l)
+  in
+    if n < 0 then invalid_arg "list_addn"
+    else aux n
+
+let list_make n v = list_addn n v []
 
 let list_assign l n e =
   let rec assrec stk = function
@@ -757,9 +762,6 @@ let rec list_skipn n l = match n,l with
 let rec list_skipn_at_least n l =
   try list_skipn n l with Failure _ -> []
 
-let rec list_addn n x l =
-  if n = 0 then l else x :: (list_addn (pred n) x l)
-
 let list_prefix_of prefl l =
   let rec prefrec = function
     | (h1::t1, h2::t2) -> h1 = h2 && prefrec (t1,t2)