IStream: a concat_map primitive.

3 files changed, 7 insertions, 2 deletions

diff --git a/lib/iStream.ml b/lib/iStream.ml
index 1d9f55998..bcb5336f2 100644
--- a/lib/iStream.ml
+++ b/lib/iStream.ml
@@ -76,3 +76,5 @@ let rec concat_node = function
 
 and concat (s : 'a t t) =
   lazy (concat_node (Lazy.force s))
+
+let concat_map f l = concat (map f l)
diff --git a/lib/iStream.mli b/lib/iStream.mli
index 9e4dec415..61967f49e 100644
--- a/lib/iStream.mli
+++ b/lib/iStream.mli
@@ -61,6 +61,9 @@ val concat : 'a t t -> 'a t
 val map_filter : ('a -> 'b option) -> 'a t -> 'b t
 (** Mixing [map] and [filter]. Not tail-rec. *)
 
+val concat_map : ('a -> 'b t) -> 'a t -> 'b t
+(** [concat_map f l] is the same as [concat (map f l)]. *)
+
 (** {6 Conversions} *)
 
 val of_list : 'a list -> 'a t
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index 1c67d4b01..8ac193fa5 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -167,7 +167,7 @@ module PatternMatching (E:StaticEnvironment) = struct
       coherent. *)
   let (>>=) (type a) (type b) (x:a m) (f:a -> b m) : b m =
     let open IStream in
-    concat (map begin fun { subst=substx; context=contextx; terms=termsx; lhs=lhsx } ->
+    concat_map begin fun { subst=substx; context=contextx; terms=termsx; lhs=lhsx } ->
       map_filter begin fun { subst=substf; context=contextf; terms=termsf; lhs=lhsf } ->
         try 
           Some { 
@@ -178,7 +178,7 @@ module PatternMatching (E:StaticEnvironment) = struct
           }
         with Not_coherent_metas -> None
       end (f lhsx)
-    end x)
+    end x
 
   (** A variant of [(>>=)] when the first argument returns [unit]. *)
   let (<*>) (type a) (x:unit m) (y:a m) : a m =