diff options
| author | soubiran | 2008-04-21 07:40:43 +0000 |
|---|---|---|
| committer | soubiran | 2008-04-21 07:40:43 +0000 |
| commit | 1c38e7101eb54594b06111271369cbffac50c3b6 (patch) | |
| tree | 5ff88aa5ea73d48b9d6d65754212ee042b59b435 /kernel | |
| parent | c82f88f9dd833dc33dacfe03822bc5987041e6ac (diff) | |
Correction bug 1838 + doc modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10821 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/modops.ml | 7 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 8d74c4c300..4d0af4fee5 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -258,8 +258,11 @@ let rec eval_struct env = function let mp = scrape_alias mp env in let sub_alias = (lookup_modtype mp env).typ_alias in let sub_alias = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias - | _ -> sub_alias in + | SEBstruct (msid,sign) -> + join_alias + (subst_key (map_msid msid mp) sub_alias) + (map_msid msid mp) + | _ -> sub_alias in let sub_alias = update_subst_alias sub_alias (map_mbid farg_id mp (None)) in let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a895e68ce7..2fffa09220 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -287,8 +287,8 @@ let add_module l me senv = check_label l senv.labset; let mb = translate_module senv.env me in let mp = MPdot(senv.modinfo.modpath, l) in - let is_functor,sub = Modops.update_subst senv.env mb mp in let env' = full_add_module mp mb senv.env in + let is_functor,sub = Modops.update_subst senv.env mb mp in mp, { old = senv.old; env = env'; modinfo = |