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

0 files changed, 0 insertions, 0 deletions