correction bug 1839

is line, and those below, will be ignored--

M    kernel/mod_subst.mli
M    kernel/mod_typing.ml
M    kernel/mod_subst.ml
M    kernel/subtyping.ml
M    kernel/modops.ml
M    library/declaremods.ml


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10849 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 42 insertions, 0 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 0df3e6631..040d7f811 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -347,6 +347,48 @@ let update_subst_alias subst1 subst2 =
   in
     Umap.fold alias_subst subst1 empty_subst
 
+let update_subst subst1 subst2 =
+ let subst_inv key (mp,resolve) l =
+    let newmp = 
+      match key with 
+	| MBI msid -> MPbound msid
+	| MSI msid -> MPself msid
+	| MPI mp -> mp
+    in
+   match mp with 
+     | MPbound mbid ->  ((MBI mbid),newmp)::l
+     | MPself msid ->  ((MSI msid),newmp)::l
+     | _ ->   ((MPI mp),newmp)::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 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
+	    in
+	    begin
+	      match List.fold_left compute_set_newkey [] subst_mbi with
+		| [] -> None
+		| l -> Some (l)
+	    end
+	| _ -> None
+    in
+      match newsetkey with
+	| None -> sub
+	| Some l -> 
+	    List.fold_left (fun s k -> Umap.add k (mp,resolve) s)
+	      sub l
+  in
+    Umap.fold alias_subst subst1 empty_subst
+
 let join_alias (subst1 : substitution) (subst2 : substitution) =
   let apply_subst (sub : substitution) key (mp,resolve) =
     let mp',resolve' =