added list_seq

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index c16b11159c38ccde56621da9d3b9c97c611419c9..fe0f417cdf88521a401a54d0ebbf41ba79ef0b58 100644 (file)
--- 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 594a80027956644cb721f3007a97c34a678adfa1..96e7a398cbe275d2148eca4ec6be0e637a3a7b23 100644 (file)
--- 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 }