From a4bd836942106154703e10805405e8b4e6eb11ee Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 25 Apr 2008 15:55:16 +0000
Subject: correction bug 1839 is line, and those below, will be ignored--

M    kernel/mod_subst.mli
M    kernel/mod_typing.ml
M    kernel/mod_subst.ml
M    kernel/subtyping.ml
M    kernel/modops.ml
M    library/declaremods.ml


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10849 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/modops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 590db27274..49e49f5731 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -329,8 +329,9 @@ and merge_with env mtb with_decl alias=
 	      match with_decl with
                   With_definition_body (_,c) -> With_definition_body (idl,c),None
 		| With_module_body (idc,mp,cst) -> 
+		    let mp' = scrape_alias mp env in
 		    With_module_body (idl,mp,cst),
-		      Some(map_mp (mp_rec (List.rev idc)) mp) 
+		      Some(map_mp (mp_rec (List.rev idc)) mp') 
 	    in
 	    let subst = match subst1 with
 	      | None -> None
-- 
cgit v1.2.3