From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 10 Jul 2006 16:50:43 +0000 (+0000)
Subject: added flatten_map
X-Git-Tag: 0.4.95@7852~1238
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63ac9d7bc2ea4690c50dfb7e6648db4698a9fe72;p=helm.git

added flatten_map
---

diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml
index 57511db0e..b36a4d89d 100644
--- a/components/extlib/hExtlib.ml
+++ b/components/extlib/hExtlib.ml
@@ -135,6 +135,10 @@ let is_alphanum c = is_alpha c || is_digit c
 
 (** {2 List processing} *)
 
+let flatten_map f l =
+  List.flatten (List.map f l)
+;;
+
 let rec list_uniq ?(eq=(=)) = function 
   | [] -> []
   | h::[] -> [h]
diff --git a/components/extlib/hExtlib.mli b/components/extlib/hExtlib.mli
index 52b74429c..a38b09334 100644
--- a/components/extlib/hExtlib.mli
+++ b/components/extlib/hExtlib.mli
@@ -78,6 +78,7 @@ val list_uniq:
 val filter_map: ('a -> 'b option) -> 'a list -> 'b list (** filter + map *)
 val list_concat: ?sep:'a list -> 'a list list -> 'a list (**String.concat-like*)
 val list_findopt: ('a -> 'b option) -> 'a list -> 'b option
+val flatten_map: ('a -> 'b list) -> 'a list -> 'b list
 
 (** {2 Debugging & Profiling} *)