summaryrefslogtreecommitdiff
path: root/checklink/Library.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checklink/Library.ml')
-rw-r--r--checklink/Library.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/checklink/Library.ml b/checklink/Library.ml
index dbe7b46..0014025 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -3,10 +3,16 @@ open BinPos
type bitstring = Bitstring.bitstring
+let is_some = function
+| Some(_) -> true
+| None -> false
+
let from_some = function
| Some(x) -> x
| None -> raise Not_found
+let filter_some l = List.(map from_some (filter is_some l))
+
type 'a on_success =
| OK of 'a
| ERR of string