diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 000b2d65e6..25889718f9 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -427,9 +427,11 @@ and strengthen_and_subst_struct let resolve_out,rest' = strengthen_and_subst_struct rest subst env mp_alias mp_from mp_to alias incl resolver in - if incl && not (con_in_delta con resolver) then + if incl then + let old_name = constant_of_delta resolver con in (add_constant_delta_resolver - (make_con_equiv mp_to mp_alias empty_dirpath l) resolve_out), + (constant_of_kn_equiv (user_con con) (canonical_con old_name)) + resolve_out), item'::rest' else resolve_out,item'::rest' @@ -439,9 +441,10 @@ and strengthen_and_subst_struct let resolve_out,rest' = strengthen_and_subst_struct rest subst env mp_alias mp_from mp_to alias incl resolver in - if incl && not (mind_in_delta mind resolver) then + if incl then + let old_name = mind_of_delta resolver mind in (add_mind_delta_resolver - (make_mind_equiv mp_to mp_alias empty_dirpath l) resolve_out), + (mind_of_kn_equiv (user_mind mind) (canonical_mind old_name)) resolve_out), item'::rest' else resolve_out,item'::rest' |