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.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index cd24bd8d0..46dac02aa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -91,10 +91,7 @@ val add_include :
module_struct_entry -> bool -> inline -> 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
-
(** Loading and saving compilation units *)