From 2d1910dc6ec51827b5ef4f05b12f0641f46a66f7 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 15 Apr 2013 19:36:51 +0000
Subject: 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
---
 kernel/safe_typing.ml  | 11 -----------
 kernel/safe_typing.mli |  3 ---
 2 files changed, 14 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a1b8204667..8518036213 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 cd24bd8d0e..46dac02aa1 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 *)
 
-- 
cgit v1.2.3