diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 7 |
1 files changed, 5 insertions, 2 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 |