1 files changed, 43 insertions, 20 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2a5d3114c2..699f6c90ee 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -492,21 +492,30 @@ let val_substituted val_a =
       [|[|val_a|];[|val_list val_subst;val_a|]|])
 
 let from_val a = ref (LSval a)
-
+ 
+let rec replace_mp_in_mp mpfrom mpto mp =
+  match mp with
+    | _ when mp = mpfrom -> mpto
+    | MPdot (mp1,l) ->
+	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
+	  if mp1==mp1' then mp
+	  else MPdot (mp1',l)
+    | _ -> mp
+
+let rec mp_in_mp mp mp1 =
+  match mp1 with
+    | _ when mp1 = mp -> true
+    | MPdot (mp2,l) -> mp_in_mp mp mp2
+    | _ -> false
+	
 let mp_in_key mp key = 
-  let rec mp_rec mp1 = 
-    match mp1 with
-      | _ when mp1 = mp -> true
-      | MPdot (mp2,l) -> mp_rec mp2
-      | _ -> false
-  in 
-    match key with
+  match key with
     | MP mp1 -> 
-	mp_rec mp1
+	mp_in_mp mp mp1
     | KN kn -> 
 	let mp1,dir,l = repr_kn kn in
-	  mp_rec mp1
-   
+	  mp_in_mp mp mp1
+  
 let subset_prefixed_by mp resolver =
   let prefixmp key hint resolv =
     if mp_in_key mp key then
@@ -583,10 +592,23 @@ let add_delta_resolver resolver1 resolver2 =
     Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
       resolver2
 
+let substition_prefixed_by k mp subst =
+  let prefixmp key (mp_to,reso) sub =
+    match key with 
+      | MPI mpk ->
+	  if mp_in_mp mp mpk && mp <> mpk then
+	    let new_key = replace_mp_in_mp mp k mpk in
+	      Umap.add (MPI new_key) (mp_to,reso) sub
+	  else 
+	    sub
+      |  _ -> sub
+  in
+    Umap.fold prefixmp subst empty_subst
+
 let join (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,resolve) =
+  let apply_subst key (mp,resolve) res =
     let mp',resolve' =
-      match subst_mp0 sub mp with
+      match subst_mp0 subst2 mp with
 	  None -> mp, None
 	| Some (mp',resolve') ->  mp'
 	    ,Some resolve' in
@@ -594,15 +616,16 @@ let join (subst1 : substitution) (subst2 : substitution) =
       match resolve' with
           Some res -> 
 	    add_delta_resolver 
-	      (subst_dom_codom_delta_resolver sub resolve)
-	      res
+	      (subst_dom_codom_delta_resolver subst2 resolve) res
 	| None -> 
-	    subst_codom_delta_resolver sub resolve
+	    subst_codom_delta_resolver subst2 resolve
     in
-      mp',resolve'' in
-  let subst = Umap.mapi (apply_subst subst2) subst1 in
-    (Umap.fold Umap.add subst2 subst)   
-
+    let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in
+    let prefixed_subst = substition_prefixed_by k mp subst2 in
+      Umap.fold Umap.add prefixed_subst 
+	(Umap.add key (mp',resolve'') res) in
+  let subst = Umap.fold apply_subst subst1 empty_subst in
+    (Umap.fold Umap.add subst2 subst) 
 
 let force fsubst r =
   match !r with