From 206ce9892fbfc2dbac151fb3479b9a0849461536 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Tue, 2 Feb 2010 15:35:21 +0000
Subject: Small fix on module inclusion.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12706 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/modops.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 000b2d65e6..25889718f9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -427,9 +427,11 @@ and strengthen_and_subst_struct
 	let resolve_out,rest' =
 	  strengthen_and_subst_struct rest subst env 
 	    mp_alias mp_from mp_to alias incl resolver in
-	  if incl && not (con_in_delta con resolver) then
+	  if incl then
+	    let old_name = constant_of_delta resolver con in
 	    (add_constant_delta_resolver
-	      (make_con_equiv mp_to mp_alias empty_dirpath l) resolve_out),
+	      (constant_of_kn_equiv (user_con con) (canonical_con old_name)) 
+	      resolve_out),
 	item'::rest'
 	  else
 	    resolve_out,item'::rest'
@@ -439,9 +441,10 @@ and strengthen_and_subst_struct
 	let resolve_out,rest' =
 	  strengthen_and_subst_struct rest subst env 
 	    mp_alias mp_from mp_to alias incl resolver in
-	  if incl && not (mind_in_delta mind resolver) then
+	  if incl then
+	    let old_name =  mind_of_delta resolver mind in 
 	    (add_mind_delta_resolver
-	      (make_mind_equiv mp_to mp_alias empty_dirpath l) resolve_out),
+	      (mind_of_kn_equiv (user_mind mind) (canonical_mind old_name)) resolve_out),
 	item'::rest'
 	  else
 	    resolve_out,item'::rest'
-- 
cgit v1.2.3