diff options
| author | soubiran | 2010-02-02 15:35:21 +0000 |
|---|---|---|
| committer | soubiran | 2010-02-02 15:35:21 +0000 |
| commit | 206ce9892fbfc2dbac151fb3479b9a0849461536 (patch) | |
| tree | a852b2d7a3ac538c6d0dc59297695eacae944780 | |
| parent | 3ef3e0d145c2765c17e0f10b9c0d896c09365662 (diff) | |
Small fix on module inclusion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12706 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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)) = |