diff options
Diffstat (limited to 'lib/util.ml')
| -rw-r--r-- | lib/util.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index ee373120e2..8b3fb2428b 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -778,6 +778,11 @@ let option_smartmap f a = match a with | None -> a | Some x -> let x' = f x in if x'==x then a else Some x' +let rec filter_some = function + | [] -> [] + | None::l -> filter_some l + | Some a::l -> a :: filter_some l + let map_succeed f = let rec map_f = function | [] -> [] |
