aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.ml (renamed from kernel/declarations.mli)0
-rw-r--r--kernel/kernel.mllib1
2 files changed, 1 insertions, 0 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.ml
index 71e228b19c..71e228b19c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.ml
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 4c540a6d73..2f49982ce2 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -42,3 +42,4 @@ Safe_typing
Vm
Csymtable
Vconv
+Declarations