Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)

 This commit should fix the contrib ProjectiveGeometry

 This update_delta_resolver is in fact a sequential composition
 (resolver1 then resolver2). The earlier version was strangely
 favoring the bindings coming from resolver2 over the bindings
 coming from (resolver1 chained with resolver2). So any inlining
 information stored in resolver1 could be discarded savagely.
 Apparently, this situation wasn't occurring in practice until
 recently, when I started to do lots of Mod_subst.join for
 improving the size of modular libobjects in the vo's.

 So, when combining two resolvers now :

 - Inline(_,None) is the weakest information, it's just a
   declaration that we intend to inline this kn someday if possible
   (i.e. when we'll have a transparent implementation for it).
   This kind of Inline is only relevant inside a module type.

 - Equiv(_) should only appear in modules (after some Include)
   so it should be ok if it takes precedence over any Inline(_,None)
   remaining in the other resolver.

 - Inline(_,Some _) is there after functor application
   (cf inline_delta_resolver) : we've done the inlining,
   so we don't care anymore about other Equiv(_) or Inline(_,None)
   informations about this kn, since we have anyway a new body
   for it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16965 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 17 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index b79276750..009bcb770 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -460,29 +460,26 @@ let subst_dom_codom_delta_resolver = gen_subst_delta_resolver true
 
 let update_delta_resolver resolver1 resolver2 =
   let mp_apply_rslv mkey mequ rslv =
-    if Deltamap.mem_mp mkey resolver2 then rslv
-    else Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv
+    Deltamap.add_mp mkey (find_prefix resolver2 mequ) rslv
   in
-  let kn_apply_rslv kkey hint rslv =
-    if Deltamap.mem_kn kkey resolver2 then rslv
-    else
-      let hint' = match hint with
-	| Equiv kequ ->
-	  (try Equiv (solve_delta_kn resolver2 kequ)
-	   with Change_equiv_to_inline (lev,c) -> Inline (lev, Some c))
-	| _ -> hint
-      in
-      Deltamap.add_kn kkey hint' rslv
+  let kn_apply_rslv kkey hint1 rslv =
+    let hint = match hint1 with
+      | Equiv kequ ->
+	(try Equiv (solve_delta_kn resolver2 kequ)
+	 with Change_equiv_to_inline (lev,c) -> Inline (lev, Some c))
+      | Inline (_,Some _) -> hint1
+      | Inline (_,None) ->
+        (try Deltamap.find_kn kkey resolver2 with Not_found -> hint1)
+    in
+    Deltamap.add_kn kkey hint rslv
   in
-  Deltamap.fold mp_apply_rslv kn_apply_rslv resolver1 empty_delta_resolver
+  Deltamap.fold mp_apply_rslv kn_apply_rslv resolver1 resolver2
 
 let add_delta_resolver resolver1 resolver2 =
-  if resolver1 == resolver2 then
-    resolver2
-  else if Deltamap.is_empty resolver2 then
+  if Deltamap.is_empty resolver2 then
     resolver1
   else
-    Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
+    update_delta_resolver resolver1 resolver2
 
 let substition_prefixed_by k mp subst =
   let mp_prefixmp kmp (mp_to,reso) sub =