From a0299ca93ea3a0243e10caec1dc6e63e464178db Mon Sep 17 00:00:00 2001
From: soubiran
Date: Thu, 3 Dec 2009 16:43:45 +0000
Subject: declaremods.ml <--- code factoring mod_subst <--- Some inlining
 informations was propagated into module implementation whereas those
 informations should stay in module type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12558 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_subst.ml    | 11 +++++++----
 library/declaremods.ml | 11 +++++++----
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 5f81ddb4da..75a167f6c5 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -527,10 +527,13 @@ let mp_in_key mp key =
    
 let subset_prefixed_by mp resolver =
   let prefixmp key hint resolv =
-    if mp_in_key mp key then
-      Deltamap.add key hint resolv
-    else 
-      resolv
+    match hint with 
+      | Inline _ -> resolv
+      | _ ->
+	  if mp_in_key mp key then
+	    Deltamap.add key hint resolv
+	  else 
+	    resolv
   in
     Deltamap.fold prefixmp resolver empty_delta_resolver
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 1644b7a7c7..46c9933c77 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -846,16 +846,19 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
 
   let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
-  let mty_entry_o, mty_sub_l = match res with
+  let env = Global.env() in
+  let mty_entry_o, subs = match res with
     | Topconstr.Enforce mty -> Some (funct interp_modtype mty), []
-    | Topconstr.Check mtys -> None, List.map (funct interp_modtype) mtys
+    | Topconstr.Check mtys -> None, build_subtypes interp_modtype mmp arg_entries mtys
   in
+ 
+  (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
   let mexpr_entry_o = Option.map (funct interp_modexpr) mexpr_o in
   let entry =
     {mod_entry_type = mty_entry_o;
      mod_entry_expr = mexpr_entry_o }
   in
-  let env = Global.env() in
+
   let substobjs =
     match entry with
       | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp mte
@@ -871,7 +874,7 @@ let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
 
   if mp_env <> mp then anomaly "Kernel and Library names do not match";
 
-  let subs = List.map (Mod_typing.translate_module_type env mp) mty_sub_l in
+  
   check_subtypes mp subs;
 
   let substobjs = (mbids,mp_env,
-- 
cgit v1.2.3