This big commit addresses two problems:

  1- Management of the name-space in a modular development / sharing of non-logical objects.
  2- Performance of atomic module operations (adding a module to the environment, subtyping ...).

1-
There are 3 module constructions which derive equalities on fields from a module to another:
Let P be a module path and foo a field of P

Module M := P.

Module M.
 Include P.
 ...
End M.

Declare Module K : S with Module M := P.

In this 3 cases we don't want to be bothered by the duplication of names. 
Of course, M.foo delta reduce to P.foo but many non-logical features of coq 
do not work modulo conversion (they use eq_constr or constr_pat object). 
To engender a transparent name-space (ie using P.foo or M.foo is the same thing) 
we quotient the name-space by the equivalence relation on names induced by the 
3 constructions above.
To implement this, the types constant and mutual_inductive are now couples of 
kernel_names. The first projection correspond to the name used by the user and the second
projection to the canonical name, for example the internal name of M.foo is
(M.foo,P.foo). 
So:
*************************************************************************************
*  Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values   *
*************************************************************************************

Map and Set indexed on names are ordered on user name for the kernel side
and on canonical name outside. Thus we have sharing of notation, hints... for free 
(also for a posteriori declaration of them, ex: a notation on M.foo will be 
avaible on P.foo). If you want to use this, use the appropriate compare function
defined in name.ml or libnames.ml.


2-
No more time explosion (i hoppe) when using modules i have re-implemented atomic
module operations so that they are all linear in the size of the module. We also
have no more unique identifier (internal module names) for modules, it is now based 
on a section_path like mechanism => we have less substitutions to perform at require,
module closing and subtyping but we pre-compute more information hence if we instanciate 
several functors then we have bigger vo.


Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions
above, i will work on it soon...



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

1 files changed, 459 insertions, 273 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 238aa3544a..a9d4a246d6 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -13,27 +13,30 @@ open Util
 open Names
 open Term
 
-(* WARNING: not every constant in the associative list domain used to exist
-   in the environment. This allows a simple implementation of the join
-   operation. However, iterating over the associative list becomes a non-sense
-*)
-type resolver = (constant * constr option) list
-
-let make_resolver resolve = resolve
-
-let apply_opt_resolver resolve kn =
- match resolve with
-    None -> None
-  | Some resolve ->
-     try List.assoc kn resolve with Not_found -> None
-
-type substitution_domain =
-    MSI of mod_self_id
+
+type delta_hint =
+    Inline of constr option
+  | Equiv of kernel_name
+  | Prefix_equiv of module_path
+
+type delta_key = 
+    KN of kernel_name
+  | MP of module_path
+
+module Deltamap =  Map.Make(struct 
+			      type t = delta_key
+			      let compare = Pervasives.compare
+			    end)
+
+type delta_resolver = delta_hint Deltamap.t
+
+let empty_delta_resolver = Deltamap.empty
+
+type substitution_domain = 
   | MBI of mod_bound_id
   | MPI of module_path
 
 let string_of_subst_domain = function
-   MSI msid -> debug_string_of_msid msid
  | MBI mbid -> debug_string_of_mbid mbid
  | MPI mp -> string_of_mp mp
 
@@ -42,48 +45,233 @@ module Umap = Map.Make(struct
 			 let compare = Pervasives.compare
 		       end)
 
-type substitution = (module_path * resolver option) Umap.t
-
+type substitution = (module_path * delta_resolver) Umap.t
+    
 let empty_subst = Umap.empty
 
-let add_msid msid mp =
-  Umap.add (MSI msid) (mp,None)
+
+let string_of_subst_domain = function
+  | MBI mbid -> debug_string_of_mbid mbid
+  | MPI mp -> string_of_mp mp
+      
 let add_mbid mbid mp resolve =
   Umap.add (MBI mbid) (mp,resolve)
-let add_mp mp1 mp2  =
-  Umap.add (MPI mp1) (mp2,None)
+let add_mp mp1 mp2 resolve =
+  Umap.add (MPI mp1) (mp2,resolve)
 
 
-let map_msid msid mp = add_msid msid mp empty_subst
 let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
-let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
+let map_mp mp1 mp2 resolve = add_mp mp1 mp2 resolve empty_subst
+
+let add_inline_delta_resolver con =
+  Deltamap.add (KN(user_con con)) (Inline None)
+    
+let add_inline_constr_delta_resolver con cstr =
+  Deltamap.add (KN(user_con con)) (Inline (Some cstr))
+
+let add_constant_delta_resolver con =
+  Deltamap.add (KN(user_con con)) (Equiv (canonical_con con))
+
+let add_mind_delta_resolver mind =
+  Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind))
+
+let add_mp_delta_resolver mp1 mp2 = 
+  Deltamap.add (MP mp1) (Prefix_equiv mp2)
+
+let mp_in_delta mp = 
+  Deltamap.mem (MP mp) 
+
+let con_in_delta con resolver = 
+try 
+  match Deltamap.find (KN(user_con con)) resolver with
+  | Inline _  | Prefix_equiv _ -> false
+  | Equiv _ -> true
+with
+ Not_found -> false
+
+let mind_in_delta mind resolver = 
+try 
+  match Deltamap.find (KN(user_mind mind)) resolver with
+  | Inline _  | Prefix_equiv _ -> false
+  | Equiv _ -> true
+with
+ Not_found -> false
+
+let delta_of_mp resolve mp =
+  try 
+    match Deltamap.find (MP mp) resolve with
+      | Prefix_equiv mp1 -> mp1
+      | _ -> anomaly "mod_subst: bad association in delta_resolver"
+  with
+      Not_found -> mp
+	
+let delta_of_kn resolve kn =
+  try 
+    match Deltamap.find (KN kn) resolve with
+      | Equiv kn1 -> kn1
+      | Inline _ -> kn
+      | _ -> anomaly 
+	  "mod_subst: bad association in delta_resolver"
+  with
+      Not_found -> kn
+
+let remove_mp_delta_resolver resolver mp =
+    Deltamap.remove (MP mp) resolver
+
+exception Inline_kn
+
+let rec find_prefix resolve mp = 
+  let rec sub_mp = function
+    | MPdot(mp,l) as mp_sup -> 
+	(try 
+	   match Deltamap.find (MP mp_sup) resolve with
+	     | Prefix_equiv mp1 -> mp1
+	     | _ -> anomaly 
+		 "mod_subst: bad association in delta_resolver"
+	 with
+	     Not_found -> MPdot(sub_mp mp,l))
+    | p -> 
+	match Deltamap.find (MP p) resolve with
+	  | Prefix_equiv mp1 -> mp1
+	  | _ -> anomaly 
+		 "mod_subst: bad association in delta_resolver"	
+  in
+    try 
+      sub_mp mp
+    with
+	Not_found -> mp
+	  
+let solve_delta_kn resolve kn =
+  try 
+      match Deltamap.find (KN kn) resolve with
+	| Equiv kn1 -> kn1
+	| Inline _ -> raise Inline_kn
+	| _ -> anomaly 
+	    "mod_subst: bad association in delta_resolver"
+  with
+      Not_found | Inline_kn -> 
+	let mp,dir,l = repr_kn kn in
+	let new_mp = find_prefix resolve mp in
+	  if mp == new_mp then 
+	    kn
+	  else
+	    make_kn new_mp dir l
+	      
+
+let constant_of_delta resolve con =
+  let kn = user_con con in
+  let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then
+      con
+    else
+      constant_of_kn_equiv kn new_kn
+	
+let constant_of_delta2 resolve con =
+  let kn = canonical_con con in
+  let kn1 = user_con con in
+  let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then
+      con
+    else
+      constant_of_kn_equiv kn1 new_kn
+
+let mind_of_delta resolve mind =
+  let kn = user_mind mind in
+  let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then
+      mind
+    else
+      mind_of_kn_equiv kn new_kn
+	
+let mind_of_delta2 resolve mind =
+  let kn = canonical_mind mind in
+  let kn1 = user_mind mind in
+  let new_kn = solve_delta_kn resolve kn in
+    if kn == new_kn then
+      mind
+    else
+      mind_of_kn_equiv kn1 new_kn
+
+
+
+let inline_of_delta resolver = 
+  let extract key hint l =
+    match key,hint with 
+      |KN kn, Inline _ -> kn::l
+      | _,_ -> l
+  in
+    Deltamap.fold extract resolver []
 
-let list_contents sub =
-  let one_pair uid (mp,_) l =
-    (string_of_subst_domain uid, string_of_mp mp)::l
+exception Not_inline
+  
+let constant_of_delta_with_inline resolve con =
+  let kn1,kn2 = canonical_con con,user_con con in
+    try
+      match Deltamap.find (KN kn2) resolve with 
+	| Inline None -> None
+	| Inline (Some const) -> Some const
+	| _ -> raise Not_inline
+    with
+	Not_found | Not_inline -> 
+	  try match Deltamap.find (KN kn1) resolve with 
+	    | Inline None -> None
+	    | Inline (Some const) -> Some const
+	    | _ -> raise Not_inline
+	  with
+	      Not_found | Not_inline -> None
+
+let string_of_key = function
+      | KN kn -> string_of_kn kn
+      | MP mp -> string_of_mp mp
+
+let string_of_hint = function
+      | Inline _ -> "inline"
+      | Equiv kn -> string_of_kn kn
+      | Prefix_equiv mp -> string_of_mp mp
+
+let debug_string_of_delta resolve =
+  let to_string key hint s = 
+    s^", "^(string_of_key key)^"=>"^(string_of_hint hint)
+  in 
+    Deltamap.fold to_string resolve ""  
+      
+let list_contents sub = 
+  let one_pair uid (mp,reso) l =
+    (string_of_subst_domain uid, string_of_mp mp,debug_string_of_delta reso)::l
   in
     Umap.fold one_pair sub []
-
+      
 let debug_string_of_subst sub =
-  let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in
+  let l = List.map (fun (s1,s2,s3) -> s1^"|->"^s2^"["^s3^"]")
+    (list_contents sub) in
     "{" ^ String.concat "; " l ^ "}"
+      
+let debug_pr_delta resolve = 
+  str (debug_string_of_delta resolve)
 
 let debug_pr_subst sub =
   let l = list_contents sub in
-  let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2)
+  let f (s1,s2,s3) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++
+			      spc () ++ str "[" ++ str s3 ++ str "]") 
   in
     str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}"
-
-
+      
+      
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with
-    | MPself sid ->
-        let mp',resolve = Umap.find (MSI sid) sub in
+    | MPfile sid -> 
+        let mp',resolve = Umap.find (MPI (MPfile sid)) sub in
          mp',resolve
     | MPbound bid ->
-        let mp',resolve = Umap.find (MBI bid) sub in
-          mp',resolve
+	begin
+	  try
+            let mp',resolve = Umap.find (MBI bid) sub in
+              mp',resolve
+	  with Not_found ->
+	    let mp',resolve = Umap.find (MPI mp) sub in
+              mp',resolve
+	end
     | MPdot (mp1,l) as mp2 ->
 	begin
 	  try
@@ -93,7 +281,6 @@ let subst_mp0 sub mp = (* 's like subst *)
 	    let mp1',resolve = aux mp1 in
 	      MPdot (mp1',l),resolve
 	end
-    | _ -> raise Not_found
  in
   try
     Some (aux mp)
@@ -104,39 +291,126 @@ let subst_mp sub mp =
     None -> mp
   | Some (mp',_) -> mp'
 
-
-let subst_kn0 sub kn =
+let subst_kn_delta sub kn =
  let mp,dir,l = repr_kn kn in
   match subst_mp0 sub mp with
-     Some (mp',_) ->
-      Some (make_kn mp' dir l)
-   | None -> None
+     Some (mp',resolve) ->
+      solve_delta_kn resolve (make_kn mp' dir l)
+   | None -> kn
+
 
 let subst_kn sub kn =
- match subst_kn0 sub kn with
-    None -> kn
-  | Some kn' -> kn'
+ let mp,dir,l = repr_kn kn in
+  match subst_mp0 sub mp with
+     Some (mp',_) ->
+      (make_kn mp' dir l)
+   | None -> kn
+
+exception No_subst
+
+type sideconstantsubst =
+  | User
+  | Canonical
+
+let subst_ind sub mind =
+  let kn1,kn2 = user_mind mind,canonical_mind mind in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,mind',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_mind_equiv mp1' mp2' dir l), resolve2 
+      in
+	match side with
+	  |User ->
+	     let mind = mind_of_delta resolve mind' in
+	       mind
+	  |Canonical ->
+	     let mind = mind_of_delta2 resolve mind' in
+	       mind
+    with 
+	No_subst -> mind
+
+let subst_mind0 sub mind =
+  let kn1,kn2 = user_mind mind,canonical_mind mind in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,mind',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_mind_equiv mp1' mp2' dir l), resolve2
+      in
+	match side with
+	  |User ->
+	     let mind = mind_of_delta resolve mind' in
+	       Some mind
+	  |Canonical ->
+	     let mind = mind_of_delta2 resolve mind' in
+	       Some mind
+    with 
+	No_subst -> Some mind
 
 let subst_con sub con =
- let mp,dir,l = repr_con con in
-  match subst_mp0 sub mp with
-     None -> con,mkConst con
-   | Some (mp',resolve) ->
-      let con' = make_con mp' dir l in
-       match apply_opt_resolver resolve con with
-          None -> con',mkConst con'
-        | Some t -> con',t
+  let kn1,kn2 = user_con con,canonical_con con in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try 
+      let side,con',resolve =   
+        match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_con_equiv mp1' mp2' dir l), resolve2 
+      in
+	match constant_of_delta_with_inline resolve con' with
+            None -> begin
+	      match side with
+	      |User ->
+	      let con = constant_of_delta resolve con' in
+		con,mkConst con
+	      |Canonical ->
+		  let con = constant_of_delta2 resolve con' in
+		con,mkConst con
+	    end
+	  | Some t -> con',t
+    with No_subst -> con , mkConst con 
+ 
 
 let subst_con0 sub con =
- let mp,dir,l = repr_con con in
-  match subst_mp0 sub mp with
-      None -> None
-    | Some (mp',resolve) ->
-	let con' = make_con mp' dir l in
-       match apply_opt_resolver resolve con with
-           None -> Some (mkConst con')
-         | Some t -> Some t
-
+  let kn1,kn2 = user_con con,canonical_con con in
+  let mp1,dir,l = repr_kn kn1 in
+  let mp2,_,_ = repr_kn kn2 in
+    try  
+      let side,con',resolve =   
+	match subst_mp0 sub mp1,subst_mp0 sub mp2 with
+	    None,None ->raise No_subst
+	  | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve
+	  | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve
+	  | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical,
+	      (make_con_equiv mp1' mp2' dir l), resolve2 
+      in
+	match constant_of_delta_with_inline resolve con' with
+	    None ->begin
+	      match side with
+	      |User ->
+	      let con = constant_of_delta resolve con' in
+		Some (mkConst con)
+	      |Canonical ->
+		  let con = constant_of_delta2 resolve con' in
+		Some (mkConst con)
+	    end
+	  | t ->  t
+    with No_subst -> Some (mkConst con) 
+		
 (* Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
    Does the user mean "Unfold X.t" or does she mean "Unfold y"
@@ -220,7 +494,7 @@ let rec map_kn f f' c =
       | _ -> c
 
 let subst_mps sub =
-  map_kn (subst_kn0 sub) (subst_con0 sub)
+  map_kn (subst_mind0 sub) (subst_con0 sub)
 
 let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
@@ -231,233 +505,145 @@ let rec replace_mp_in_mp mpfrom mpto mp =
 	  else MPdot (mp1',l)
     | _ -> mp
 
-let replace_mp_in_con mpfrom mpto kn =
- let mp,dir,l = repr_con kn in
+let replace_mp_in_kn mpfrom mpto kn =
+ let mp,dir,l = repr_kn kn in
   let mp'' = replace_mp_in_mp mpfrom mpto mp in
     if mp==mp'' then kn
-    else make_con mp'' dir l
-
-exception BothSubstitutionsAreIdentitySubstitutions
-exception ChangeDomain of resolver
-
-let join (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,resolve) =
-    let mp',resolve' =
-      match subst_mp0 sub mp with
-	  None -> mp, None
-	| Some (mp',resolve') -> mp',resolve' in
-    let resolve'' : resolver option =
-      try
-	let res =
-	  match resolve with
-              Some res -> res
-	    | None ->
-		match resolve' with
-		    None -> raise BothSubstitutionsAreIdentitySubstitutions
-		  | Some res -> raise (ChangeDomain res)
-	in
-	  Some
-	    (List.map
-               (fun (kn,topt) ->
-		  kn,
-		  match topt with
-		      None ->
-			(match key with
-			     MSI msid ->
-			       let kn' = replace_mp_in_con (MPself msid) mp kn in
-				 apply_opt_resolver resolve' kn'
-			   | MBI mbid ->
-			       let kn' = replace_mp_in_con (MPbound mbid) mp kn in
-				 apply_opt_resolver resolve' kn'
-			   | MPI mp1 ->
-			       let kn' = replace_mp_in_con mp1 mp kn in
-				 apply_opt_resolver resolve' kn')
-		    | Some t -> Some (subst_mps sub t)) res)
-      with
-	  BothSubstitutionsAreIdentitySubstitutions -> None
-	| ChangeDomain res ->
-	    let rec changeDom = function
-	      | [] -> []
-	      | (kn,topt)::r ->
-		  let key' =
-		    match key with
-			MSI msid -> MPself msid
-                      | MBI mbid -> MPbound mbid
-		      | MPI mp1 -> mp1 in
-		  let kn' = replace_mp_in_con mp key' kn in
-		    if kn==kn' then
-		      (*the key does not appear in kn, we remove it
-			from the resolver that we are building*)
-		      changeDom r
-		    else
-		      (kn',topt)::(changeDom r)
-	    in
-	      Some (changeDom res)
-    in
-      mp',resolve'' in
-  let subst = Umap.mapi (apply_subst subst2) subst1 in
-    (Umap.fold Umap.add subst2 subst)
-
-let subst_key subst1 subst2 =
-  let replace_in_key key (mp,resolve) sub=
-    let newkey =
-      match key with
-	| MPI mp1 ->
-	    begin
-	      match subst_mp0 subst1 mp1 with
-		| None -> None
-		| Some (mp2,_) -> Some (MPI mp2)
-	    end
-	| _ -> None
-    in
-      match newkey with
-	| None -> Umap.add key (mp,resolve) sub
-	| Some mpi -> Umap.add mpi (mp,resolve) sub
+    else make_kn mp'' dir l
+
+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
+    | MP mp1 -> 
+	mp_rec mp1
+    | KN kn -> 
+	let mp1,dir,l = repr_kn kn in
+	  mp_rec mp1
+   
+let subset_prefixed_by mp resolver =
+  let prefixmp key hint resolv =
+    if mp_in_key mp key then
+      Deltamap.add key hint resolv
+    else 
+      resolv
   in
-    Umap.fold replace_in_key subst2 empty_subst
-
-let update_subst_alias subst1 subst2 =
- let subst_inv key (mp,resolve) sub =
-    let newmp =
-      match key with
-	| MBI msid -> MPbound msid
-	| MSI msid -> MPself msid
-	| MPI mp -> mp
-    in
-   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
+    Deltamap.fold prefixmp resolver empty_delta_resolver
+
+let subst_dom_delta_resolver subst resolver =
+  let apply_subst key hint resolver =
+    match key with
+	(MP mp) ->
+	  Deltamap.add (MP (subst_mp subst mp)) hint resolver
+      | (KN kn) ->
+	  Deltamap.add (KN (subst_kn subst kn)) hint resolver
   in
-  let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
-  let alias_subst key (mp,resolve) sub=
-    let newkey =
-      match key with
-	| MPI mp1 ->
-	    begin
-	      match subst_mp0 subst_mbi mp1 with
-		| None -> None
-		| Some (mp2,_) -> Some (MPI mp2)
-	    end
-	| _ -> None
-    in
-      match newkey with
-	| None -> Umap.add key (mp,resolve) sub
-	| Some mpi -> Umap.add mpi (mp,resolve) sub
+    Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let subst_mp_delta sub mp key=
+ match subst_mp0 sub mp with
+    None -> empty_delta_resolver,mp
+  | Some (mp',resolve) -> 
+      let mp1 = find_prefix resolve mp' in
+      let resolve1 = subset_prefixed_by mp1 resolve in
+	match key with
+	    MP mpk ->
+	      (subst_dom_delta_resolver 
+		 (map_mp mp1 mpk empty_delta_resolver) resolve1),mp1
+	  | _ -> anomaly "Mod_subst: Bad association in resolver" 
+
+let subst_codom_delta_resolver subst resolver =
+  let apply_subst key hint resolver =
+    match hint with
+	Prefix_equiv mp ->
+	  let derived_resolve,mpnew = subst_mp_delta subst mp key in
+	    Deltamap.fold Deltamap.add derived_resolve
+	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
+      | (Equiv kn) ->
+	  Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+      | Inline None ->
+	  Deltamap.add key hint resolver
+      | Inline (Some t) ->
+	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
   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,resolve)::l
-     | MPself msid ->  ((MSI msid),newmp,resolve)::l
-     | _ ->   ((MPI mp),newmp,resolve)::l
+    Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let subst_dom_codom_delta_resolver subst resolver =
+  let apply_subst key hint resolver =
+    match key,hint with
+	(MP mp1),Prefix_equiv mp ->
+	  let key = MP (subst_mp subst mp1) in
+	  let derived_resolve,mpnew = subst_mp_delta subst mp key in
+	    Deltamap.fold Deltamap.add derived_resolve
+	      (Deltamap.add key (Prefix_equiv mpnew) resolver)
+      | (KN kn1),(Equiv kn) ->
+	  let key = KN (subst_kn subst kn1) in
+	  Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver
+      | (KN kn),Inline None ->
+	  let key = KN (subst_kn subst kn) in
+	  Deltamap.add key hint resolver
+      | (KN kn),Inline (Some t) ->
+	  let key = KN (subst_kn subst kn) in
+	  Deltamap.add key (Inline (Some (subst_mps subst t))) resolver
+      | _,_ -> anomaly "Mod_subst: Bad association in resolver" 
   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',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,resolve)::l
-	    in
-	    begin
-	      match List.fold_left compute_set_newkey [] subst_mbi with
-		| [] -> None
-		| l -> Some (l)
-	    end
-	| _ -> None
+    Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let update_delta_resolver resolver1 resolver2 =
+ let apply_res key hint res = 
+      try
+	match hint with
+	    Prefix_equiv mp ->
+	      let new_hint =
+		Prefix_equiv (find_prefix resolver2 mp)
+	      in Deltamap.add key new_hint res
+	  | Equiv kn ->
+	      let new_hint =
+		Equiv (solve_delta_kn resolver2 kn)
+	      in Deltamap.add key new_hint res
+	  | _ -> Deltamap.add key hint res
+      with not_found -> 
+	Deltamap.add key hint res
     in
-      match newsetkey with
-	| None -> sub
-	| Some l ->
-	    List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s)
-	      sub l
-  in
-    Umap.fold alias_subst subst1 empty_subst
+      Deltamap.fold apply_res resolver1 empty_delta_resolver
+
+let add_delta_resolver resolver1 resolver2 =
+  if resolver1 == resolver2 then
+    resolver2
+  else if resolver2 = empty_delta_resolver then
+    resolver1
+  else
+    Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
+      resolver2
 
-let join_alias (subst1 : substitution) (subst2 : substitution) =
+let join (subst1 : substitution) (subst2 : substitution) =
   let apply_subst (sub : substitution) key (mp,resolve) =
     let mp',resolve' =
       match subst_mp0 sub mp with
 	  None -> mp, None
-	| Some (mp',resolve') -> mp',resolve' in
-    let resolve'' : resolver option =
-      try
-	let res =
-	  match resolve with
-              Some res -> res
-	    | None ->
-		match resolve' with
-		    None -> raise BothSubstitutionsAreIdentitySubstitutions
-		  | Some res -> raise (ChangeDomain res)
-	in
-	  Some
-	    (List.map
-               (fun (kn,topt) ->
-		  kn,
-		  match topt with
-		      None ->
-			(match key with
-			     MSI msid ->
-			       let kn' = replace_mp_in_con (MPself msid) mp kn in
-				 apply_opt_resolver resolve' kn'
-			   | MBI mbid ->
-			       let kn' = replace_mp_in_con (MPbound mbid) mp kn in
-				 apply_opt_resolver resolve' kn'
-			   | MPI mp1 ->
-			       let kn' = replace_mp_in_con mp1 mp kn in
-				 apply_opt_resolver resolve' kn')
-		    | Some t -> Some (subst_mps sub t)) res)
-      with
-	  BothSubstitutionsAreIdentitySubstitutions -> None
-	| ChangeDomain res ->
-	    let rec changeDom = function
-	      | [] -> []
-	      | (kn,topt)::r ->
-		  let key' =
-		    match key with
-			MSI msid -> MPself msid
-                      | MBI mbid -> MPbound mbid
-		      | MPI mp1 -> mp1 in
-		  let kn' = replace_mp_in_con mp key' kn in
-		    if kn==kn' then
-		      (*the key does not appear in kn, we remove it
-			from the resolver that we are building*)
-		      changeDom r
-		    else
-		      (kn',topt)::(changeDom r)
-	    in
-	      Some (changeDom res)
+	| Some (mp',resolve') ->  mp'
+	    ,Some resolve' in
+    let resolve'' : delta_resolver =
+      match resolve' with
+          Some res -> 
+	    add_delta_resolver 
+	      (subst_dom_codom_delta_resolver sub resolve)
+	      res
+	| None -> 
+	    subst_codom_delta_resolver sub resolve
     in
       mp',resolve'' in
-  Umap.mapi (apply_subst subst2) subst1
+  let subst = Umap.mapi (apply_subst subst2) subst1 in
+    (Umap.fold Umap.add subst2 subst)   
 
-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
-  | MSI sid,MPself sid' -> sid = sid'
   | MBI bid,MPbound bid' -> bid = bid'
   | _,MPdot (mp1,_) -> occur_in_path uid mp1
   | _ -> false
@@ -471,7 +657,7 @@ let occur_uid uid sub =
       false
     with Exit -> true
 
-let occur_msid uid = occur_uid (MSI uid)
+
 let occur_mbid uid = occur_uid (MBI uid)
 
 type 'a lazy_subst =