diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2016-10-10 10:53:51 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-10 11:05:22 +0200 |
commit | c70fe0c63238128a6bb98b9fa75445c4b71c7af5 (patch) | |
tree | e8a0897676d8dc4cefc6e9d4d8f0166fe6a1366b /lib | |
parent | eb87cdaeb252d758b6a76b36867254823169576b (diff) |
Fix #4416: - Incorrect "Error: Incorrect number of goals"
In `Ftactic` the number of results could desynchronise with the number
of goals when some goals were solved by side effect in a different
branch of a `DISPATCH`.
See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
Diffstat (limited to 'lib')
-rw-r--r-- | lib/monad.ml | 11 | ||||
-rw-r--r-- | lib/monad.mli | 3 |
2 files changed, 14 insertions, 0 deletions
diff --git a/lib/monad.ml b/lib/monad.ml index a1714a41b..2e55e9698 100644 --- a/lib/monad.ml +++ b/lib/monad.ml @@ -64,6 +64,9 @@ module type ListS = sig its second argument in a tail position. *) val iter : ('a -> unit t) -> 'a list -> unit t + (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*) + val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t + (** {6 Two-list iterators} *) @@ -138,6 +141,14 @@ module Make (M:Def) : S with type +'a t = 'a M.t = struct | a::b::l -> f a >> f b >> iter f l + let rec map_filter f = function + | [] -> return [] + | a::l -> + f a >>= function + | None -> map_filter f l + | Some b -> + map_filter f l >>= fun filtered -> + return (b::filtered) let rec fold_left2 r f x l1 l2 = match l1,l2 with diff --git a/lib/monad.mli b/lib/monad.mli index c8655efa0..f7de71f53 100644 --- a/lib/monad.mli +++ b/lib/monad.mli @@ -66,6 +66,9 @@ module type ListS = sig its second argument in a tail position. *) val iter : ('a -> unit t) -> 'a list -> unit t + (** Like the regular {!CList.map_filter}. The monadic effects are threaded left*) + val map_filter : ('a -> 'b option t) -> 'a list -> 'b list t + (** {6 Two-list iterators} *) |