From 920926c8bded37b057ba0c59f0144a085a1bb35e Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 26 Mar 2008 13:22:04 +0000
Subject: 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
---
 kernel/mod_subst.ml  | 8 ++++++++
 kernel/mod_subst.mli | 2 ++
 2 files changed, 10 insertions(+)

(limited to 'kernel')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 3b3d280900..0df3e66317 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 b54ae6f3b4..5384d0f85a 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
-- 
cgit v1.2.3