aboutsummaryrefslogtreecommitdiff
path: root/lib/util.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/util.ml')
-rw-r--r--lib/util.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml
index 8798842837..c4229fd322 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -1211,6 +1211,11 @@ let iterate_for a b f x =
let rec iterate i v = if i > b then v else iterate (succ i) (f i v) in
iterate a x
+let app_opt f x =
+ match f with
+ | Some f -> f x
+ | None -> x
+
(* Delayed computations *)
type 'a delayed = unit -> 'a