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 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'kernel')

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
 
-- 
cgit v1.2.3