diff options
| -rw-r--r-- | kernel/modops.ml | 11 | ||||
| -rw-r--r-- | library/declare.ml | 2 |
2 files changed, 8 insertions, 5 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' diff --git a/library/declare.ml b/library/declare.ml index ffe53e505f..dce84ff043 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -106,7 +106,7 @@ let load_constant i ((sp,kn),(_,_,kind)) = (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn),_) = - let con = constant_of_kn kn in + let con = Global.constant_of_delta (constant_of_kn kn) in Nametab.push (Nametab.Exactly i) sp (ConstRef con) let cache_constant ((sp,kn),(cdt,dhyps,kind)) = |