diff options
| -rw-r--r-- | kernel/mod_subst.ml | 12 | ||||
| -rw-r--r-- | kernel/modops.ml | 6 | ||||
| -rw-r--r-- | library/declaremods.ml | 47 |
3 files changed, 32 insertions, 33 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 040d7f811e..2ac7b623b4 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -356,23 +356,23 @@ let update_subst subst1 subst2 = | MPI mp -> mp in match mp with - | MPbound mbid -> ((MBI mbid),newmp)::l - | MPself msid -> ((MSI msid),newmp)::l - | _ -> ((MPI mp),newmp)::l + | MPbound mbid -> ((MBI mbid),newmp,resolve)::l + | MPself msid -> ((MSI msid),newmp,resolve)::l + | _ -> ((MPI mp),newmp,resolve)::l in let subst_mbi = Umap.fold subst_inv subst2 [] in let alias_subst key (mp,resolve) sub= let newsetkey = match key with | MPI mp1 -> - let compute_set_newkey l (k,mp') = + let compute_set_newkey l (k,mp',resolve) = let mp_from_key = match k with | MBI msid -> MPbound msid | MSI msid -> MPself msid | MPI mp -> mp in let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in - if new_mp1 == mp1 then l else (MPI new_mp1)::l + if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l in begin match List.fold_left compute_set_newkey [] subst_mbi with @@ -384,7 +384,7 @@ let update_subst subst1 subst2 = match newsetkey with | None -> sub | Some l -> - List.fold_left (fun s k -> Umap.add k (mp,resolve) s) + List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s) sub l in Umap.fold alias_subst subst1 empty_subst diff --git a/kernel/modops.ml b/kernel/modops.ml index f904bab548..8febff5e85 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -273,9 +273,9 @@ let rec eval_struct env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - let sub_alias1 = update_subst sub_alias - (map_mbid farg_id mp (None)) in - let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in + let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in + let sub_alias1 = update_subst sub_alias + (map_mbid farg_id mp (Some resolve)) in eval_struct env (subst_struct_expr (join sub_alias1 (map_mbid farg_id mp (Some resolve))) fbody_b) diff --git a/library/declaremods.ml b/library/declaremods.ml index 7923f566b3..d8808b6dbb 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -643,26 +643,26 @@ let rec get_modtype_substobjs env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - let sub3= - if sub1 = empty_subst then - update_subst sub_alias (map_mbid farg_id mp None) - else - let sub1' = join_alias sub1 (map_mbid farg_id mp None) in - let sub_alias' = update_subst sub_alias sub1' in - join sub1' sub_alias' - in - let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in - let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in + let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in (match mbids with | mbid::mbids -> let resolve = Modops.resolver_of_environment farg_id farg_b mp sub_alias env in + let sub3= + if sub1 = empty_subst then + update_subst sub_alias (map_mbid farg_id mp None) + else + let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub_alias' = update_subst sub_alias sub1' in + join sub1' sub_alias' + in + let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in (* application outside the kernel, only for substitutive objects (that are all non-logical objects) *) - ((join - (join subst sub3) - (map_mbid mbid mp (Some resolve))) - , mbids, msid, objs) + ((join + (join subst sub3) + (map_mbid mbid mp (Some resolve))) + , mbids, msid, objs) | [] -> match mexpr with | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") @@ -952,21 +952,20 @@ let rec get_module_substobjs env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - - let sub3= - if sub1 = empty_subst then - update_subst sub_alias (map_mbid farg_id mp None) - else - let sub1' = join_alias sub1 (map_mbid farg_id mp None) in - let sub_alias' = update_subst sub_alias sub1' in - join sub1' sub_alias' - in - let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> let resolve = Modops.resolver_of_environment farg_id farg_b mp sub_alias env in + let sub3= + if sub1 = empty_subst then + update_subst sub_alias (map_mbid farg_id mp None) + else + let sub1' = join_alias sub1 (map_mbid farg_id mp None) in + let sub_alias' = update_subst sub_alias sub1' in + join sub1' sub_alias' + in + let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in (* application outside the kernel, only for substitutive objects (that are all non-logical objects) *) ((join |