aboutsummaryrefslogtreecommitdiffhomepage
path: root/clib/clib.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'clib/clib.mllib')
-rw-r--r--clib/clib.mllib1
1 files changed, 1 insertions, 0 deletions
diff --git a/clib/clib.mllib b/clib/clib.mllib
index 0b5d9826f..c9b4d72fc 100644
--- a/clib/clib.mllib
+++ b/clib/clib.mllib
@@ -5,6 +5,7 @@ CEphemeron
Hashset
Hashcons
+OrderedType
CSet
CMap
CList