aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.mli')
-rw-r--r--kernel/safe_typing.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f011d42b7..169fd158d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -89,8 +89,10 @@ val end_modtype :
label -> safe_environment -> module_path * safe_environment
val add_include :
- module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment
+ module_struct_entry -> bool -> safe_environment ->
+ delta_resolver * safe_environment
+val pack_module : safe_environment -> module_body
val current_modpath : safe_environment -> module_path
val delta_of_senv : safe_environment -> delta_resolver*delta_resolver