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, 478 insertions, 237 deletions

diff --git a/checker/declarations.ml b/checker/declarations.ml
index 0066e7848..3211cc28f 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -31,60 +31,241 @@ let val_cst_type =
 
 
 type substitution_domain =
-    MSI of mod_self_id
   | MBI of mod_bound_id
   | MPI of module_path
 
 let val_subst_dom =
-  val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
+  val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|]
 
 module Umap = Map.Make(struct
 			 type t = substitution_domain
 			 let compare = Pervasives.compare
 		       end)
 
-type resolver
 
-type substitution = (module_path * resolver option) Umap.t
+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 = (module_path * delta_resolver) Umap.t
 type 'a subst_fun = substitution -> 'a -> 'a
 
-let val_res = val_opt no_val
+let val_res_dom = no_val
+  (*val_sum "resolver_domain" 0 [|[|val_kn|];[|val_mp|]|]*)
+
+let val_res = no_val
+ (* val_map ~name:"delta_resolver"
+    val_res_dom  
+    (val_sum "resolver_codomain" 0 [|[|val_opt val_constr||];[|val_kn|];[|val_mp|]|])*)
 
 let val_subst =
   val_map ~name:"substitution"
     val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
 
 
-let fold_subst fs fb fp =
+let fold_subst fb fp =
   Umap.fold
     (fun k (mp,_) acc ->
       match k with
-          MSI msid -> fs msid mp acc
         | MBI mbid -> fb mbid mp acc
         | MPI mp1 -> fp mp1 mp acc)
 
 let empty_subst = Umap.empty
 
-let add_msid msid mp =
-  Umap.add (MSI msid) (mp,None)
 let add_mbid mbid mp =
-  Umap.add (MBI mbid) (mp,None)
+  Umap.add (MBI mbid) (mp,empty_delta_resolver)
 let add_mp mp1 mp2  =
-  Umap.add (MPI mp1) (mp2,None)
+  Umap.add (MPI mp1) (mp2,empty_delta_resolver)
 
-let map_msid msid mp = add_msid msid mp empty_subst
 let map_mbid mbid mp = add_mbid mbid mp empty_subst
 let map_mp mp1 mp2 = add_mp mp1 mp2 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 []
+
+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 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
@@ -94,59 +275,135 @@ 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)
   with Not_found -> None
 
-
-
-let subst_mp0 sub mp = (* 's like subst *)
- let rec aux mp =
-  match mp with
-    | MPself sid -> fst (Umap.find (MSI sid) sub)
-    | MPbound bid -> fst (Umap.find (MBI bid) sub)
-    | MPdot (mp1,l) as mp2 ->
-	begin
-	  try fst (Umap.find (MPI mp2) sub)
-	  with Not_found -> MPdot (aux mp1,l)
-	end
-
-    | _ -> raise Not_found
- in
-  try Some (aux mp) with Not_found -> None
-
 let subst_mp sub mp =
  match subst_mp0 sub mp with
     None -> mp
-  | Some mp' -> 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
-   | Some mp' -> make_con mp' dir l
+  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,Const con
+	      |Canonical ->
+		  let con = constant_of_delta2 resolve con' in
+		con,Const con
+	    end
+	  | Some t -> con',t
+    with No_subst -> con , Const con 
+ 
 
 let subst_con0 sub con =
- let mp,dir,l = repr_con con in
-  match subst_mp0 sub mp with
-      None -> None
-    | Some mp' ->
-	let con' = make_con mp' dir l in
-        Some (Const con')
+  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 (Const con)
+	      |Canonical ->
+		  let con = constant_of_delta2 resolve con' in
+		Some (Const con)
+	    end
+	  | t ->  t
+    with No_subst -> Some (Const con)
+
 
 let rec map_kn f f' c =
   let func = map_kn f f' in
@@ -220,22 +477,8 @@ 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
-    | _ 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 replace_mp_in_con mpfrom mpto kn =
- let mp,dir,l = kn in
-  let mp'' = replace_mp_in_mp mpfrom mpto mp in
-    if mp==mp'' then kn
-    else (mp'', dir, l)
 
 type 'a lazy_subst =
   | LSval of 'a
@@ -253,117 +496,115 @@ let force fsubst r =
       r := LSval a';
       a'
 
-
-
-let join (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,_) =
-      match subst_mp0 sub mp with
-	  None -> mp,None
-	| Some mp' -> mp',None 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 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 sub
-	| Some mpi -> Umap.add mpi mp sub
+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,_) sub =
-    let newmp =
-      match key with
-	| MBI msid -> Some (MPbound msid)
-	| MSI msid -> Some (MPself msid)
-	| _ -> None
-    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
+    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,_) 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,None) sub
-	| Some mpi -> Umap.add mpi (mp,None) sub
-  in
-    Umap.fold alias_subst subst1 empty_subst
+    Deltamap.fold apply_subst resolver empty_delta_resolver
 
-let join_alias (subst1 : substitution) (subst2 : substitution) =
-  let apply_subst (sub : substitution) key (mp,_) =
-      match subst_mp0 sub mp with
-	  None -> mp,None
-	| Some mp' -> mp',None in
-  Umap.mapi (apply_subst subst2) subst1
-
-
-let update_subst subst1 subst2 =
- let subst_inv key (mp,_) 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
+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) 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
-  let subst_mbi = Umap.fold subst_inv subst2 [] in
-  let alias_subst key (mp,_) 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
+    Deltamap.fold apply_subst resolver empty_delta_resolver
+
+let subst_dom_codom_delta_resolver subst resolver =
+  subst_dom_delta_resolver subst
+    (subst_codom_delta_resolver subst 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 -> Umap.add k (mp,None) 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
+    Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
+      resolver2
 
+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'
+	    ,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
+  let subst = Umap.mapi (apply_subst subst2) subst1 in
+    (Umap.fold Umap.add subst2 subst)   
 
 let subst_substituted s r =
   match !r with
@@ -414,7 +655,7 @@ let val_recarg = val_sum "recarg" 1 (* Norec *)
 
 let subst_recarg sub r = match r with
   | Norec | Mrec _  -> r
-  | Imbr (kn,i) -> let kn' = subst_kn sub kn in
+  | Imbr (kn,i) -> let kn' = subst_ind sub kn in
       if kn==kn' then r else Imbr (kn',i)
 
 type wf_paths = recarg Rtree.t
@@ -547,8 +788,6 @@ type mutual_inductive_body = {
   (* Universes constraints enforced by the inductive declaration *)
     mind_constraints : Univ.constraints;
 
-  (* Source of the inductive block when aliased in a module *)
-    mind_equiv : kernel_name option
   }
 let val_ind_pack = val_tuple "mutual_inductive_body"
   [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
@@ -605,8 +844,7 @@ let subst_mind sub mib =
     mind_params_ctxt =
       map_rel_context (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
-    mind_constraints = mib.mind_constraints ;
-    mind_equiv = Option.map (subst_kn sub) mib.mind_equiv }
+    mind_constraints = mib.mind_constraints  }
 
 (* Modules *)
 
@@ -616,7 +854,6 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * struct_expr_body option * Univ.constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -624,116 +861,120 @@ and structure_body = (label * structure_field_body) list
 and struct_expr_body =
   | SEBident of module_path
   | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body
-  | SEBstruct of mod_self_id * structure_body
-  | SEBapply of struct_expr_body * struct_expr_body
-      * Univ.constraints
+  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
+  | SEBstruct of structure_body
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path *
-      struct_expr_body option * Univ.constraints
+    With_module_body of identifier list * module_path
   | With_definition_body of  identifier list * constant_body
 
 and module_body =
-    { mod_expr : struct_expr_body option;
-      mod_type : struct_expr_body option;
+    { mod_mp : module_path;
+      mod_expr : struct_expr_body option; 
+      mod_type : struct_expr_body;
+      mod_type_alg : struct_expr_body option;
       mod_constraints : Univ.constraints;
-      mod_alias : substitution;
+      mod_delta : delta_resolver;
       mod_retroknowledge : action list}
 
 and module_type_body =
-    { typ_expr : struct_expr_body;
-      typ_strength : module_path option;
-      typ_alias : substitution}
+    { typ_mp : module_path;
+      typ_expr : struct_expr_body;
+      typ_expr_alg : struct_expr_body option ;
+      typ_constraints : Univ.constraints;
+      typ_delta :delta_resolver}
 
 (* the validation functions: *)
 let rec val_sfb o = val_sum "struct_field_body" 0
   [|[|val_cb|];       (* SFBconst *)
     [|val_ind_pack|]; (* SFBmind *)
     [|val_module|];   (* SFBmodule *)
-    [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *)
     [|val_modtype|]   (* SFBmodtype *)
   |] o
 and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o
 and val_seb o = val_sum "struct_expr_body" 0
   [|[|val_mp|];                      (* SEBident *)
     [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *)
-    [|val_uid;val_sb|];              (* SEBstruct *)
+    [|val_sb|];              (* SEBstruct *)
     [|val_seb;val_seb;val_cstrs|];   (* SEBapply *)
     [|val_seb;val_with|]             (* SEBwith *)
   |] o
 and val_with o = val_sum "with_declaration_body" 0
-  [|[|val_list val_id;val_mp;val_cstrs|];
+  [|[|val_list val_id;val_mp|];
     [|val_list val_id;val_cb|]|] o
 and val_module o = val_tuple "module_body"
-  [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
+  [|val_mp;val_opt val_seb;val_opt val_seb;
+    val_seb;val_cstrs;val_res;no_val|] o
 and val_modtype o = val_tuple "module_type_body"
-  [|val_seb;val_opt val_mp;val_subst|] o
+  [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o
 
 
 let rec subst_with_body sub = function
-  | With_module_body(id,mp,typ_opt,cst) ->
-      With_module_body(id,subst_mp sub mp,
-		       Option.smartmap (subst_struct_expr sub) typ_opt,cst)
+  | With_module_body(id,mp) ->
+      With_module_body(id,subst_mp sub mp)
   | With_definition_body(id,cb) ->
       With_definition_body( id,subst_const_body sub cb)
 
-and subst_modtype sub mtb =
+and subst_modtype sub mtb=
   let typ_expr' = subst_struct_expr sub mtb.typ_expr in
-    if typ_expr'==mtb.typ_expr then
-      mtb
+  let typ_alg' = 
+    Option.smartmap 
+      (subst_struct_expr sub) mtb.typ_expr_alg in
+  let mp = subst_mp sub mtb.typ_mp
+  in
+    if typ_expr'==mtb.typ_expr && 
+      typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then
+	mtb
     else
-      { mtb with
-	  typ_expr = typ_expr'}
-
-and subst_structure sub sign =
-  let subst_body  = function
-      SFBconst cb ->
+      {mtb with 
+	 typ_mp = mp;
+	 typ_expr = typ_expr';
+	 typ_expr_alg = typ_alg'}
+
+and subst_structure sub sign = 
+  let subst_body = function
+      SFBconst cb -> 
 	SFBconst (subst_const_body sub cb)
-    | SFBmind mib ->
+    | SFBmind mib -> 
 	SFBmind (subst_mind sub mib)
-    | SFBmodule mb ->
-	SFBmodule (subst_module sub mb)
-    | SFBmodtype mtb ->
+    | SFBmodule mb -> 
+	SFBmodule (subst_module sub  mb)
+    | SFBmodtype mtb -> 
 	SFBmodtype (subst_modtype sub mtb)
- | SFBalias (mp,typ_opt ,cst) ->
-	SFBalias (subst_mp sub mp,
-		  Option.smartmap (subst_struct_expr sub) typ_opt,cst)
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
-and subst_module  sub mb =
-  let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in
-  (* This is similar to the previous case. In this case we have
-     a module M in a signature that is knows to be equivalent to a module M'
-     (because the signature is "K with Module M := M'") and we are substituting
-     M' with some M''. *)
-  let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in
-  let mb_alias = join_alias mb.mod_alias sub in
-    if mtb'==mb.mod_type && mb.mod_expr == me'
-      && mb_alias == mb.mod_alias
-    then mb else
-      { mod_expr = me';
-	mod_type=mtb';
-	mod_constraints=mb.mod_constraints;
-	mod_alias = mb_alias;
-	mod_retroknowledge=mb.mod_retroknowledge}
 
+and subst_module sub mb =
+  let mtb' = subst_struct_expr sub mb.mod_type in
+  let typ_alg' = Option.smartmap 
+    (subst_struct_expr sub ) mb.mod_type_alg in
+  let me' = Option.smartmap 
+    (subst_struct_expr sub) mb.mod_expr in
+  let mp = subst_mp sub mb.mod_mp in
+     if mtb'==mb.mod_type && mb.mod_expr == me' 
+       && mp == mb.mod_mp
+    then mb else
+      { mb with
+	  mod_mp = mp;
+	  mod_expr = me';
+	  mod_type_alg = typ_alg';
+	  mod_type=mtb'}
 
 and subst_struct_expr sub = function
-    | SEBident mp -> SEBident (subst_mp sub  mp)
-    | SEBfunctor (msid, mtb, meb') ->
-	SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb')
-    | SEBstruct (msid,str)->
-	SEBstruct(msid, subst_structure sub str)
+    | SEBident mp -> SEBident (subst_mp sub mp)
+    | SEBfunctor (mbid, mtb, meb') -> 
+	SEBfunctor(mbid,subst_modtype sub mtb
+		     ,subst_struct_expr sub meb')
+    | SEBstruct (str)->
+	SEBstruct( subst_structure sub  str)
     | SEBapply (meb1,meb2,cst)->
 	SEBapply(subst_struct_expr sub meb1,
 		 subst_struct_expr sub meb2,
 		 cst)
-    | SEBwith (meb,wdb)->
+    | SEBwith (meb,wdb)-> 
 	SEBwith(subst_struct_expr sub meb,
 		subst_with_body sub wdb)
 
 
-let subst_signature_msid msid mp =
-  subst_structure (map_msid msid mp)