summaryrefslogtreecommitdiff
path: root/checklink/Library.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checklink/Library.ml')
-rw-r--r--checklink/Library.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/checklink/Library.ml b/checklink/Library.ml
index 67d8a45..bb0d217 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -3,6 +3,8 @@ open BinPos
type bitstring = Bitstring.bitstring
+module StringMap = Map.Make (String)
+
let is_some: 'a option -> bool = function
| Some(_) -> true
| None -> false