aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-26 13:22:04 +0000
committerGravatar soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-26 13:22:04 +0000
commit920926c8bded37b057ba0c59f0144a085a1bb35e (patch)
treec9b4f56c28aeef27217167c610a2d57f5392d3f6
parent0e6f439bac7c9dc5598d311c14db8e7049f66e0c (diff)
Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-dehors du noyau et
sont donc independantes des substitutions engendrees par les alias de module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10720 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--kernel/mod_subst.ml8
-rw-r--r--kernel/mod_subst.mli2
-rw-r--r--library/declaremods.ml1
3 files changed, 11 insertions, 0 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 3b3d28090..0df3e6631 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -404,6 +404,14 @@ let join_alias (subst1 : substitution) (subst2 : substitution) =
mp',resolve'' in
Umap.mapi (apply_subst subst2) subst1
+let remove_alias subst =
+ let rec remove key (mp,resolve) sub =
+ match key with
+ MPI _ -> sub
+ | _ -> Umap.add key (mp,resolve) sub
+ in
+ Umap.fold remove subst empty_subst
+
let rec occur_in_path uid path =
match uid,path with
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index b54ae6f3b..5384d0f85 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -88,3 +88,5 @@ val update_subst_alias : substitution -> substitution -> substitution
val subst_key : substitution -> substitution -> substitution
val join_alias : substitution -> substitution -> substitution
+
+val remove_alias : substitution -> substitution
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 80944b2e6..7c228741b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -770,6 +770,7 @@ let classify_import (_,(export,_ as obj)) =
if export then Substitute obj else Dispose
let subst_import (_,subst,(export,mp as obj)) =
+ let subst = remove_alias subst in
let mp' = subst_mp subst mp in
if mp'==mp then obj else
(export,mp')