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 /kernel/modops.ml | |
| 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
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' |