module Reduction (debut)

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

1 files changed, 15 insertions, 1 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 625ceed870..77a26062db 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -76,7 +76,21 @@ let list_chop n l =
     | (_, []) -> failwith "chop_list"
   in 
   chop_aux [] (n,l)
- 
+
+let list_tabulate f len = 
+  let rec tabrec n =
+    if n = len then [] else (f n)::(tabrec (n+1))
+  in 
+  tabrec 0
+
+let list_assign l n e = 
+  let rec assrec stk = function
+    | ((h::t), 0) -> List.rev_append stk (e::t)
+    | ((h::t), n) -> assrec (h::stk) (t, n-1)
+    | ([], _) -> failwith "list_assign"
+  in 
+  assrec [] (l,n)
+
 (* Arrays *)
 
 let array_exists f v =