From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Sep 2008 12:47:09 +0000 (+0000)
Subject: added list_seq
X-Git-Tag: make_still_working~4758
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ff5d621723a60609c67152c110b8386f7902c1ff;p=helm.git

added list_seq
---

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index c16b11159..fe0f417cd 100644
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -520,3 +520,12 @@ let rec mk_list x = function
   | 0 -> []
   | n -> x :: mk_list x (n-1)
 ;;
+
+let list_seq start stop =
+  let rec aux pos =
+    if pos = stop then []
+    else pos :: (aux (pos+1))
+  in
+    aux start
+;;
+
diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 594a80027..96e7a398c 100644
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -109,6 +109,9 @@ val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -
 val split_nth: int -> 'a list -> 'a list * 'a list
 
 val mk_list: 'a -> int -> 'a list
+
+(* makes the list [start; ...; stop - 1] *)
+val list_seq: int -> int -> int list
 (** {2 Debugging & Profiling} *)
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }