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, 0 insertions, 5 deletions
diff --git a/lib/util.ml b/lib/util.ml
index cfb4ebabc2..531e4fe7d6 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -105,11 +105,6 @@ let app_opt f x =
| Some f -> f x
| None -> x
-let un_opt x default =
- match x with
- | None -> default
- | Some y -> y
-
(* Stream *)
let stream_nth n st =