From 7dfb5d517e932b1b42445e4b1413dca72693cc4d Mon Sep 17 00:00:00 2001
From: soubiran
Date: Tue, 25 Mar 2008 16:55:10 +0000
Subject: Correction de bugs relatifs a la compostion des substitutions
 engendrees par les alias de module

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10718 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_subst.ml | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

(limited to 'kernel/mod_subst.ml')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ea477d6a15..3b3d280900 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -320,16 +320,14 @@ let update_subst_alias subst1 subst2 =
  let subst_inv key (mp,resolve) sub =
     let newmp = 
       match key with 
-	| MBI msid -> Some (MPbound msid)
-	| MSI msid -> Some (MPself msid)
-	| _ -> None
+	| MBI msid -> MPbound msid
+	| MSI msid -> MPself msid
+	| MPI mp -> mp
     in
-      match newmp with
-	| None -> sub
-	| Some mpi -> match mp with 
-	    | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub
-	    | MPself msid -> Umap.add (MSI msid) (mpi,None) sub
-	    | _ ->  Umap.add (MPI mp) (mpi,None) sub
+   match mp with 
+     | MPbound mbid -> Umap.add (MBI mbid) (newmp,None) sub
+     | MPself msid -> Umap.add (MSI msid) (newmp,None) sub
+     | _ ->  Umap.add (MPI mp) (newmp,None) sub
   in 
   let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
   let alias_subst key (mp,resolve) sub=
-- 
cgit v1.2.3