diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-11 14:35:13 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-11 14:35:13 +0000 |
| commit | 07b85674ef5f90467ea9bd8ed3c87572d2af8016 (patch) | |
| tree | 8a064d76b6ea922cd77aef80bf9b7341929c961e /library/declaremods.ml | |
| parent | cbe2466edde3811ebeee9da59cba56ab600de39c (diff) | |
Correction bug alias d'alias.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11107 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index bb6d947c5..1b0cd86ae 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -1066,17 +1066,19 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = mod_entry_expr = Some (MSEident mp) } -> let dir,mp' = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in let (sub,mbids,msid,objs) = substobjs in - let prefix = dir,(mp',empty_dirpath) in let mp1 = Environ.scrape_alias mp env in + let prefix = dir,(mp1,empty_dirpath) in let substituted = match mbids with | [] -> Some (subst_objects prefix - (join sub (join (map_msid msid mp') (map_mp mp' mp1))) objs) + (join sub (join (map_msid msid mp1) (map_mp mp' mp1))) objs) | _ -> None in ignore (add_leaf id - (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted))); + (in_module_alias (Some ({mod_entry_type = None; + mod_entry_expr = Some (MSEident mp1) }, mty_sub_o), + substobjs, substituted))); mmp | _ -> let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in |