From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 4 Jul 2009 13:28:35 +0200
Subject: Imported Upstream version 8.2.pl1+dfsg

---
 kernel/mod_subst.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'kernel/mod_subst.ml')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index ab4b8e47..9a76922b 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mod_subst.ml 10849 2008-04-25 15:55:16Z soubiran $ *)
+(* $Id: mod_subst.ml 11924 2009-02-13 13:51:54Z soubiran $ *)
 
 open Pp
 open Util
@@ -250,11 +250,11 @@ let join (subst1 : substitution) (subst2 : substitution) =
       try
 	let res =
 	  match resolve with
-              Some res -> res
-	    | None ->
+	    |None -> begin
 		match resolve' with
 		    None -> raise BothSubstitutionsAreIdentitySubstitutions
-		  | Some res -> raise (ChangeDomain res)
+		  | Some res -> raise (ChangeDomain res) end
+	    | Some res -> res
 	in
 	  Some
 	    (List.map
@@ -356,23 +356,23 @@ let update_subst subst1 subst2 =
 	| MPI mp -> mp
     in
    match mp with 
-     | MPbound mbid ->  ((MBI mbid),newmp)::l
-     | MPself msid ->  ((MSI msid),newmp)::l
-     | _ ->   ((MPI mp),newmp)::l
+     | MPbound mbid ->  ((MBI mbid),newmp,resolve)::l
+     | MPself msid ->  ((MSI msid),newmp,resolve)::l
+     | _ ->   ((MPI mp),newmp,resolve)::l
   in 
   let subst_mbi = Umap.fold subst_inv subst2 [] in
   let alias_subst key (mp,resolve) sub=
     let newsetkey = 
       match key with
 	| MPI mp1 -> 
-	    let compute_set_newkey l (k,mp') = 
+	    let compute_set_newkey l (k,mp',resolve) = 
 	      let mp_from_key = match k with
 		  	| MBI msid -> MPbound msid
 			| MSI msid -> MPself msid
 			| MPI mp -> mp
 	      in
 	      let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
-		if new_mp1 == mp1 then l else (MPI new_mp1)::l
+		if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l
 	    in
 	    begin
 	      match List.fold_left compute_set_newkey [] subst_mbi with
@@ -384,7 +384,7 @@ let update_subst subst1 subst2 =
       match newsetkey with
 	| None -> sub
 	| Some l -> 
-	    List.fold_left (fun s k -> Umap.add k (mp,resolve) s)
+	    List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s)
 	      sub l
   in
     Umap.fold alias_subst subst1 empty_subst
-- 
cgit v1.2.3