aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-15 19:36:51 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-15 19:36:51 +0000
commit2d1910dc6ec51827b5ef4f05b12f0641f46a66f7 (patch)
tree6e9204285e694307e23f097d35e1f604c2f0ca5b /kernel
parentebaecfe6c1e84fa3615b295dad85cbf4318a4c75 (diff)
Minor simplifications in Declaremods and Safe_typing
- get_module_substobjs (resp. modtype) without useless mp_from arg - no need for the whole Safe_typing.pack_module - ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16407 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r--kernel/safe_typing.ml11
-rw-r--r--kernel/safe_typing.mli3
2 files changed, 0 insertions, 14 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a1b820466..851803621 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -616,7 +616,6 @@ let end_modtype l senv =
local_retroknowledge =
senv.local_retroknowledge@oldsenv.local_retroknowledge}
-let current_modpath senv = senv.modinfo.modpath
let delta_of_senv senv = senv.modinfo.resolver,senv.modinfo.resolver_of_param
(* Check that the engagement expected by a library matches the initial one *)
@@ -679,16 +678,6 @@ let start_library dir senv =
loads = [];
local_retroknowledge = [] }
-let pack_module senv =
- {mod_mp=senv.modinfo.modpath;
- mod_expr=None;
- mod_type= SEBstruct (List.rev senv.revstruct);
- mod_type_alg=None;
- mod_constraints=empty_constraint;
- mod_delta=senv.modinfo.resolver;
- mod_retroknowledge=[];
- }
-
let export senv dir =
let modinfo = senv.modinfo in
begin
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 *)