aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/stateid.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-03-13 15:59:02 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-03-13 16:04:33 +0100
commit223c68e38e217d9457c476d5534b6aaf0ad2caf6 (patch)
treedb26ed390c710db8f9848283914216d037fa104b /lib/stateid.ml
parentc9b1caaa5516d616e400faa7a7c0278c8677c51c (diff)
Stateid: export a Set module
Diffstat (limited to 'lib/stateid.ml')
-rw-r--r--lib/stateid.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 1eac4bf3f..09cc2b7e8 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -36,3 +36,6 @@ let get exn = Exninfo.get exn state_id_info
let equal = Int.equal
let compare = Int.compare
+
+module Set = Set.Make(struct type t = int let compare = compare end)
+