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

16 files changed, 461 insertions, 644 deletions

diff --git a/library/declare.ml b/library/declare.ml
index da723aa4b..1084aa07d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -100,12 +100,14 @@ let load_constant i ((sp,kn),(_,_,kind)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant"
       (pr_id (basename sp) ++ str " already exists");
-  Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn));
-  add_constant_kind (constant_of_kn kn) kind
-
+  let con = Global.constant_of_delta (constant_of_kn kn) in
+    Nametab.push (Nametab.Until i) sp (ConstRef con);
+    add_constant_kind con kind
+      
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
-  Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
+  let con = constant_of_kn kn in
+    Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   let id = basename sp in
@@ -187,6 +189,7 @@ let declare_inductive_argument_scopes kn mie =
 
 let inductive_names sp kn mie =
   let (dp,_) = repr_path sp in
+  let kn = Global.mind_of_delta (mind_of_kn kn) in
   let names, _ =
     List.fold_left
       (fun (names, n) ind ->
@@ -228,17 +231,18 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
   let kn' = Global.add_mind dir id mie in
-  assert (kn'=kn);
-  add_section_kn kn (Global.lookup_mind kn').mind_hyps;
+  assert (kn'= mind_of_kn kn);
+  add_section_kn kn' (Global.lookup_mind kn').mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names;
   List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie)
 
 
 let discharge_inductive ((sp,kn),(dhyps,mie)) =
-  let mie = Global.lookup_mind kn in
+  let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+  let mie = Global.lookup_mind mind in
   let repl = replacement_context () in
-  let sechyps = section_segment_of_mutual_inductive kn in
+  let sechyps = section_segment_of_mutual_inductive mind in
   Some (discharged_hyps kn sechyps,
         Discharge.process_inductive (named_of_variable_context sechyps) repl mie)
 
@@ -271,8 +275,9 @@ let declare_mind isrecord mie =
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives" in
   let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
-  declare_mib_implicits kn;
-  declare_inductive_argument_scopes kn mie;
+  let mind = (Global.mind_of_delta (mind_of_kn kn)) in
+  declare_mib_implicits mind;
+  declare_inductive_argument_scopes mind mie;
   !xml_declare_inductive (isrecord,oname);
   oname
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index d796a2906..548a9b0f3 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -22,7 +22,7 @@ open Mod_subst
 (* modules and components *)
 
 
-(* This type is a functional closure of substitutive lib_objects.
+(* OBSOLETE This type is a functional closure of substitutive lib_objects.
 
    The first part is a partial substitution (which will be later
    applied to lib_objects when completed).
@@ -41,7 +41,7 @@ open Mod_subst
 
 *)
 type substitutive_objects =
-    substitution * mod_bound_id list * mod_self_id * lib_objects
+     mod_bound_id list * module_path * lib_objects
 
 
 (* For each module, we store the following things:
@@ -77,9 +77,10 @@ let modtab_objects =
 
 (* currently started interactive module (if any) - its arguments (if it
    is a functor) and declared output type *)
-let openmod_info =
-  ref (([],None,None) : mod_bound_id list * module_struct_entry option
-                                          * struct_expr_body option)
+let openmod_info = 
+  ref ((MPfile(initial_dir),[],None,None) 
+	 : module_path *  mod_bound_id list * module_struct_entry option 
+                                          * module_type_body option) 
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
@@ -99,7 +100,8 @@ let _ = Summary.declare_summary "MODULE-INFO"
 	    Summary.init_function = (fun () ->
 				       modtab_substobjs := MPmap.empty;
 				       modtab_objects := MPmap.empty;
-				       openmod_info := ([],None,None);
+				       openmod_info := ((MPfile(initial_dir),
+							 [],None,None));
 				       library_cache := Dirmap.empty) }
 
 (* auxiliary functions to transform full_path and kernel_name given
@@ -116,50 +118,18 @@ let dir_of_sp sp =
   let dir,id = repr_path sp in
     add_dirpath_suffix dir id
 
-let msid_of_mp = function
-    MPself msid -> msid
-  | _ -> anomaly "'Self' module path expected!"
-
-let msid_of_prefix (_,(mp,sec)) =
-  if sec=empty_dirpath then
-    msid_of_mp mp
-  else
-    anomaly ("Non-empty section in module name!" ^
-	     string_of_mp mp ^ "." ^ string_of_dirpath sec)
-
-let scrape_alias mp =
-  Environ.scrape_alias mp (Global.env())
-
 
 (* This function checks if the type calculated for the module [mp] is
    a subtype of [sub_mtb]. Uses only the global environment. *)
 let check_subtypes mp sub_mtb =
   let env = Global.env () in
-  let mtb = Environ.lookup_modtype mp env in
-  let sub_mtb =
-    {typ_expr = sub_mtb;
-    typ_strength = None;
-    typ_alias = empty_subst} in
-  let _ = Environ.add_constraints
-	    (Subtyping.check_subtypes env mtb sub_mtb)
+  let mb = Environ.lookup_module mp env in
+  let mtb = Modops.module_type_of_module env None mb in
+  let _ = Environ.add_constraints 
+    (Subtyping.check_subtypes env mtb sub_mtb) 
   in
     ()  (* The constraints are checked and forgot immediately! *)
 
-let compute_subst_objects mp (subst,mbids,msid,objs) =
-  match mbids with
-  | [] ->
-      let subst' = join_alias (map_msid msid mp) subst in
-      Some (join (map_msid msid mp) (join subst' subst), objs)
-  | _ ->
-      None
-
-let subst_substobjs dir mp substobjs =
-  match compute_subst_objects mp substobjs with
-  | Some (subst, objs) ->
-	let prefix = dir,(mp,empty_dirpath) in
-	Some (subst_objects prefix subst objs)
-  | None -> None
-
 (* These functions register the visibility of the module and iterates
    through its components. They are called by plenty module functions *)
 
@@ -178,12 +148,12 @@ let compute_visibility exists what i dir dirinfo =
       errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists")
     else
       Nametab.Until i
-
+(*
 let do_load_and_subst_module i dir mp substobjs keep =
   let prefix = (dir,(mp,empty_dirpath)) in
   let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
   let vis = compute_visibility false "load_and_subst" i dir dirinfo in
-  let objects = compute_subst_objects mp substobjs in
+  let objects = compute_subst_objects mp substobjs resolver in
   Nametab.push_dir vis dir dirinfo;
   modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
   match objects with
@@ -194,55 +164,33 @@ let do_load_and_subst_module i dir mp substobjs keep =
       Some (seg@keep)
   | None ->
       None
+*)
 
-let do_module exists what iter_objects i dir mp substobjs objects =
+let do_module exists what iter_objects i dir mp substobjs keep=
   let prefix = (dir,(mp,empty_dirpath)) in
   let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
   let vis = compute_visibility exists what i dir dirinfo in
     Nametab.push_dir vis dir dirinfo;
     modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
-    match objects with
-	Some seg ->
-	  modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects;
-	  iter_objects (i+1) prefix seg
-      | None ->  ()
+    match substobjs with
+	([],mp1,objs) -> 
+	  modtab_objects := MPmap.add mp (prefix,objs@keep) !modtab_objects;
+	  iter_objects (i+1) prefix (objs@keep)  
+      | (mbids,_,_) ->  ()
 
 let conv_names_do_module exists what iter_objects i
-      (sp,kn) substobjs substituted =
+      (sp,kn) substobjs =
   let dir,mp = dir_of_sp sp, mp_of_kn kn in
-  do_module exists what iter_objects i dir mp substobjs substituted
+  do_module exists what iter_objects i dir mp substobjs []
 
 (* Interactive modules and module types cannot be recached! cache_mod*
    functions can be called only once (and "end_mod*" set the flag to
    false then)
 *)
-
-let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) =
-  let _ = match entry with
-    | None ->
-	anomaly "You must not recache interactive modules!"
-    | Some (me,sub_mte_o) ->
-	let sub_mtb_o = match sub_mte_o with
-	    None -> None
-	  | Some mte -> Some (Mod_typing.translate_struct_entry
-				(Global.env()) mte)
-	in
-
-	let mp = Global.add_module (basename sp) me in
-	  if mp <> mp_of_kn kn then
-	    anomaly "Kernel and Library names do not match";
-
-	  match sub_mtb_o with
-	      None -> ()
-	    | Some (sub_mtb,sub) ->
-		check_subtypes mp sub_mtb
-
-  in
-  conv_names_do_module false "cache" load_objects 1 oname substobjs substituted
-
-
-
-
+let cache_module ((sp,kn),(entry,substobjs)) =
+  let dir,mp = dir_of_sp sp, mp_of_kn kn in
+    do_module false "cache" load_objects 1 dir mp substobjs []
+    
 (* TODO: This check is not essential *)
 let check_empty s = function
      | None -> ()
@@ -253,42 +201,26 @@ let check_empty s = function
 (* When this function is called the module itself is already in the
    environment. This function loads its objects only *)
 
-let load_module i (oname,(entry,substobjs,substituted)) =
+let load_module i (oname,(entry,substobjs)) =
   (* TODO: This check is not essential *)
   check_empty "load_module" entry;
-  conv_names_do_module false "load" load_objects i oname substobjs substituted
+  conv_names_do_module false "load" load_objects i oname substobjs
 
 
-let open_module i (oname,(entry,substobjs,substituted)) =
+let open_module i (oname,(entry,substobjs)) =
   (* TODO: This check is not essential *)
   check_empty "open_module" entry;
-  conv_names_do_module true "open" open_objects i oname substobjs substituted
+  conv_names_do_module true "open" open_objects i oname substobjs
 
 
 
-let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
+let subst_module (subst,(entry,(mbids,mp,objs))) =
   check_empty "subst_module" entry;
-  let dir,mp = dir_of_sp sp, mp_of_kn kn in
-  let (sub,mbids,msid,objs) = substobjs in
-  let sub = subst_key subst sub in
-  let sub' = update_subst_alias subst sub in
-  let sub' = update_subst_alias sub' (map_msid msid mp) in
- (* let sub = join_alias sub sub' in*)
-  let sub = join sub' sub in
-  let subst' = join sub subst in
-  (* substitutive_objects get the new substitution *)
-  let substobjs = (subst',mbids,msid,objs) in
-  (* if we are not a functor - calculate substitued.
-     We add "msid |-> mp" to the substitution *)
-  let substituted = subst_substobjs dir mp substobjs
-  in
-    (None,substobjs,substituted)
-
-
-let classify_module (_,substobjs,_) =
-  Substitute (None,substobjs,None)
+    (None,(mbids,subst_mp subst mp, subst_objects subst objs))
 
 
+let classify_module (_,substobjs) =
+  Substitute (None,substobjs)
 
 let (in_module,out_module) =
   declare_object {(default_object "MODULE") with
@@ -298,168 +230,6 @@ let (in_module,out_module) =
     subst_function = subst_module;
     classify_function = classify_module }
 
-
-let rec replace_alias modalias_obj obj =
-  let rec put_alias (id_alias,obj_alias) l =
-    match l with
-	[] -> []
-      | (id,o)::r
-	  when ( object_tag o = "MODULE") ->
-	  if id = id_alias then
-(*	    let (entry,subst_o,substed_o) = out_module_alias obj_alias in
-	    let (entry',subst_o',substed_o') = out_module o in
-	      begin
-		match substed_o,substed_o' with
-		    Some a,Some b ->
-		      (id,in_module_alias
-			 (entry,subst_o',Some (dump_alias_object a b)))::r*)
-	    (id_alias,obj_alias)::r
-		 (* | _,_ -> (id,o)::r
-	      end*)
-	  else (id,o)::(put_alias (id_alias,obj_alias) r)
-      | e::r -> e::(put_alias (id_alias,obj_alias) r) in
-  let rec choose_obj_alias list_alias list_obj =
-    match list_alias with
-      | [] -> list_obj
-      | o::r ->choose_obj_alias r (put_alias o list_obj) in
-    choose_obj_alias modalias_obj obj
-
-and dump_alias_object alias_obj obj =
-  let rec alias_in_obj seg =
-    match seg with
-      | [] -> []
-      | (id,o)::r when (object_tag o = "MODULE ALIAS") ->
-	  (id,o)::(alias_in_obj r)
-      | e::r -> (alias_in_obj r) in
-  let modalias_obj = alias_in_obj alias_obj in
-    replace_alias modalias_obj obj
-
-and do_module_alias exists what iter_objects i dir mp alias substobjs objects =
-  let prefix = (dir,(alias,empty_dirpath)) in
-  let alias_objects =
-    try Some (MPmap.find alias !modtab_objects) with
-	Not_found -> None in
-  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
-  let vis = compute_visibility exists what i dir dirinfo in
-    Nametab.push_dir vis dir dirinfo;
-    modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
-    match alias_objects,objects with
-	Some (_,seg), Some seg' ->
-	  let new_seg = dump_alias_object seg seg' in
-	  modtab_objects := MPmap.add mp (prefix,new_seg) !modtab_objects;
-	  iter_objects (i+1) prefix new_seg
-      | _,_->  ()
-
-and cache_module_alias ((sp,kn),(entry,substobjs,substituted)) =
-  let dir,mp,alias = match entry with
-    | None ->
-	anomaly "You must not recache interactive modules!"
-    | Some (me,sub_mte_o) ->
-	let sub_mtb_o = match sub_mte_o with
-	    None -> None
-	  | Some mte -> Some (Mod_typing.translate_struct_entry
-				(Global.env()) mte)
-	in
-
-	let mp' = match me with
-	  | {mod_entry_type = None;
-	     mod_entry_expr = Some (MSEident mp)} ->
-	      Global.add_alias (basename sp) mp
-	  | _ -> anomaly "cache module alias"
-	in
-	  if mp' <> mp_of_kn kn then
-	    anomaly "Kernel and Library names do not match";
-
-	  let _ = match sub_mtb_o with
-	      None -> ()
-	    | Some (sub_mtb,sub) ->
-	      check_subtypes mp' sub_mtb in
-	    match me with
-	      | {mod_entry_type = None;
-		 mod_entry_expr = Some (MSEident mp)} ->
-		    dir_of_sp sp,mp_of_kn kn,scrape_alias mp
-	      | _ -> anomaly "cache module alias"
-  in
-    do_module_alias false "cache" load_objects 1 dir mp alias substobjs substituted
-
-and load_module_alias i ((sp,kn),(entry,substobjs,substituted)) =
-  let dir,mp,alias=
-    match entry with
-      | Some (me,_)->
-	  begin
-	    match me with
-	      |{mod_entry_type = None;
-		mod_entry_expr = Some (MSEident mp)} ->
-		 dir_of_sp sp,mp_of_kn kn,scrape_alias mp
-	      | _ -> anomaly "Modops: Not an alias"
-	  end
-      | None -> anomaly "Modops: Empty info"
-  in
-    do_module_alias false "load" load_objects i dir mp alias substobjs substituted
-
-and open_module_alias i ((sp,kn),(entry,substobjs,substituted)) =
-  let dir,mp,alias=
-    match entry with
-      | Some (me,_)->
-	  begin
-	    match me with
-	      |{mod_entry_type = None;
-		mod_entry_expr = Some (MSEident mp)} ->
-		 dir_of_sp sp,mp_of_kn kn,scrape_alias mp
-	      | _ -> anomaly "Modops: Not an alias"
-	  end
-      | None -> anomaly "Modops: Empty info"
-  in
-    do_module_alias true "open" open_objects i dir mp alias substobjs substituted
-
-and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
-  let dir,mp = dir_of_sp sp, mp_of_kn kn in
-  let (sub,mbids,msid,objs) = substobjs in
-  let sub' = update_subst_alias subst (map_msid msid mp) in
-  let subst' = join sub' subst in
-  let subst' = join sub subst' in
-  (* substitutive_objects get the new substitution *)
-  let substobjs = (subst',mbids,msid,objs) in
-  (* if we are not a functor - calculate substitued.
-     We add "msid |-> mp" to the substitution *)
-    match entry with
-      | Some (me,sub)->
-	  begin
-	    match me with
-	      |{mod_entry_type = None;
-		mod_entry_expr = Some (MSEident mp')} ->
-		 let mp' = subst_mp subst' mp' in
-		 let mp' = scrape_alias mp' in
-		   (Some ({mod_entry_type = None;
-			 mod_entry_expr =
-			      Some (MSEident mp')},sub),
-		    substobjs, match mbids with
-		      | [] -> let subst = update_subst subst' (map_mp mp' mp) in
-			  Some (subst_objects (dir,(mp',empty_dirpath))
-				  (join (join subst' subst) (join (map_msid msid mp')
-						  (map_mp mp mp')))
-				   objs)
-
-		      | _ -> None)
-
-	      | _ -> anomaly "Modops: Not an alias"
-	  end
-      | None -> anomaly "Modops: Empty info"
-
-and classify_module_alias (entry,substobjs,_) =
-  Substitute (entry,substobjs,None)
-
-let (in_module_alias,out_module_alias) =
-  declare_object {(default_object "MODULE ALIAS") with
-		    cache_function = cache_module_alias;
-		    open_function = open_module_alias;
-		    classify_function = classify_module_alias;
-		    subst_function = subst_module_alias;
-		    load_function = load_module_alias }
-
-
-
-
 let cache_keep _ = anomaly "This module should not be cached!"
 
 let load_keep i ((sp,kn),seg) =
@@ -553,9 +323,9 @@ let open_modtype i ((sp,kn),(entry,_)) =
 
   Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn)
 
-let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) =
+let subst_modtype (subst,(entry,(mbids,mp,objs))) =
   check_empty "subst_modtype" entry;
-  (entry,(join subs subst,mbids,msid,objs))
+  (entry,(mbids,subst_mp subst mp,subst_objects subst objs))
 
 
 let classify_modtype (_,substobjs) =
@@ -571,147 +341,143 @@ let (in_modtype,_) =
       classify_function = classify_modtype }
 
 
-
-let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp =
-  let rec mp_rec = function
-    | [] -> MPself msid
-	| i::r -> MPdot(mp_rec r,label_of_id i)
-  in
-    if mbids<>[] then
+let rec replace_module_object idl ( mbids, mp, lib_stack) (mbids2,mp2,objs) mp1=
+  if mbids<>[] then 
     error "Unexpected functor objects"
-    else
-      let rec replace_idl = function
-	| _,[] -> []
-	| id::idl,(id',obj)::tail when id = id' ->
-	    let tag = object_tag obj in
-	    if tag = "MODULE" or tag ="MODULE ALIAS" then
-              (match idl with
-		   [] -> (id, in_module_alias (Some
-						 ({mod_entry_type = None;
-						   mod_entry_expr = Some (MSEident mp)},None)
-						 ,modobjs,None))::tail
-		 | _ ->
-		     let (a,substobjs,_) =  if tag =  "MODULE ALIAS" then
-		       out_module_alias obj else out_module obj in
-                     let substobjs' = replace_module_object idl substobjs modobjs mp in
-		       if tag =  "MODULE ALIAS" then
-                       (id, in_module_alias (a,substobjs',None))::tail
-		       else
-			 (id, in_module (None,substobjs',None))::tail
-              )
-	    else error "MODULE expected!"
-	| idl,lobj::tail -> lobj::replace_idl (idl,tail)
-      in
-	(join (map_mp (mp_rec (List.rev idl)) mp) subst, mbids, msid, replace_idl (idl,lib_stack))
-
-let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) =
-  (subst, mbids1@mbids2, msid, lib_stack)
-
-let rec get_modtype_substobjs env = function
-    MSEident ln -> MPmap.find ln !modtypetab
+  else
+    let rec replace_idl = function 
+      | _,[] -> [] 
+      | id::idl,(id',obj)::tail when id = id' ->
+	  if object_tag obj = "MODULE" then
+           (match idl with
+               [] -> (id, in_module 
+			(None,(mbids,(MPdot(mp,label_of_id id)),subst_objects 
+				 (map_mp mp1 (MPdot(mp,label_of_id id)) empty_delta_resolver) objs)))::tail
+             | _ ->
+               let (_,substobjs) = out_module obj in
+                let substobjs' = replace_module_object idl substobjs 
+		  (mbids2,mp2,objs) mp in
+                  (id, in_module (None,substobjs'))::tail
+           )
+	  else error "MODULE expected!"
+      | idl,lobj::tail -> lobj::replace_idl (idl,tail)
+    in
+      (mbids, mp, replace_idl (idl,lib_stack))
+
+let discr_resolver mb  = 
+     match mb.mod_type with
+	SEBstruct _ -> 
+	  Some mb.mod_delta
+      | _ -> (*case mp is a functor *)
+	  None
+
+(* Small function to avoid module typing during substobjs retrivial  *)
+let rec get_objs_modtype_application env = function
+| MSEident mp -> 
+    MPmap.find mp !modtypetab,Environ.lookup_modtype mp env,[]
+| MSEapply (fexpr, MSEident mp) -> 
+    let objs,mtb,mp_l= get_objs_modtype_application env fexpr in
+      objs,mtb,mp::mp_l
+| MSEapply (_,mexpr) ->
+    Modops.error_application_to_not_path mexpr
+| _ -> error "Application of a non-functor."
+
+let rec get_modtype_substobjs env mp_from= function
+    MSEident ln -> 
+      MPmap.find ln !modtypetab 
   | MSEfunctor (mbid,_,mte) ->
-      let (subst, mbids, msid, objs) = get_modtype_substobjs env mte in
-	(subst, mbid::mbids, msid, objs)
-  | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty
-  | MSEwith (mty, With_Module (idl,mp)) ->
-      let substobjs = get_modtype_substobjs env mty in
-      let mp = Environ.scrape_alias mp env in
-      let modobjs = MPmap.find mp !modtab_substobjs in
-	replace_module_object idl substobjs modobjs mp
-  | MSEapply (mexpr, MSEident mp) ->
-     let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in
-      let farg_id, farg_b, fbody_b = Modops.destr_functor env
-	(Modops.eval_struct env ftb) in
-      let mp = Environ.scrape_alias mp env in
-      let sub_alias = (Environ.lookup_modtype mp env).typ_alias in
-      let sub_alias = match Modops.eval_struct env (SEBident mp) with
-	| SEBstruct (msid,sign) -> join_alias
-	    (subst_key (map_msid msid mp) sub_alias)
-	      (map_msid msid mp)
-	| _ -> sub_alias in
-      let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
-	(match mbids with
-	   | mbid::mbids ->
-               let resolve =
-		 Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
-	       let sub3=
-		 if sub1 = empty_subst then
-		   update_subst sub_alias (map_mbid farg_id mp None)
-		 else
-		   let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
-		   let sub_alias' =  update_subst sub_alias sub1' in
-		     join sub1' sub_alias'
-	       in
-	       let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
-		 (* application outside the kernel, only for substitutive
-                    objects (that are all non-logical objects) *)
-		 ((join
-		     (join subst sub3)
-		     (map_mbid mbid mp (Some resolve)))
-		    , mbids, msid, objs)
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments")
+      let (mbids, mp, objs) = get_modtype_substobjs env mp_from mte in
+	(mbid::mbids, mp, objs)
+  | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mp_from mty
+  | MSEwith (mty, With_Module (idl,mp1)) -> 
+      let substobjs = get_modtype_substobjs env mp_from mty in
+      let modobjs = MPmap.find mp1 !modtab_substobjs in
+	replace_module_object idl substobjs modobjs mp1
+  | MSEapply (fexpr, MSEident mp) ->
+      let (mbids, mp1, objs),mtb_mp1,mp_l =  
+	get_objs_modtype_application env (MSEapply(fexpr, MSEident mp)) in
+      let rec compute_subst mbids sign mp_l =
+	match mbids,mp_l with
+	    [],[] -> [],empty_subst
+	  | mbid,[] -> mbid,empty_subst
+	  | [],r -> error ("Application of a functor with too few arguments.")
+	  | mbid::mbids,mp::mp_l ->
+	      let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+	      let mb = Environ.lookup_module mp env in
+	      let mp_delta = discr_resolver mb in
+	      let mbid_left,subst=compute_subst mbids fbody_b mp_l in
+		if mp_delta = None then
+		  mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst 
+		else
+		  let mp_delta = Modops.complete_inline_delta_resolver env mp 
+		    farg_id farg_b (Option.get mp_delta) in
+		    mbid_left,join (map_mbid mbid mp mp_delta) subst
+      in
+      let mbids_left,subst = compute_subst mbids mtb_mp1.typ_expr (List.rev mp_l) in
+	(mbids_left, mp1,subst_objects subst objs)
   | MSEapply (_,mexpr) ->
       Modops.error_application_to_not_path mexpr
 
-
 (* push names of bound modules (and their components) to Nametab *)
 (* add objects associated to them *)
 let process_module_bindings argids args =
   let process_arg id (mbid,mty) =
     let dir = make_dirpath [id] in
     let mp = MPbound mbid in
-    let substobjs = get_modtype_substobjs (Global.env()) mty in
-    ignore (do_load_and_subst_module 1 dir mp substobjs [])
-  in
-    List.iter2 process_arg argids args
-
+    let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mp mty in
+    let substobjs = (mbids,mp,subst_objects 
+		       (map_mp mp_from mp empty_delta_resolver) objs)in
+      do_module false "start" load_objects 1 dir mp substobjs []
+    in
+      List.iter2 process_arg argids args
+	
 let intern_args interp_modtype (idl,arg) =
   let lib_dir = Lib.library_dp() in
   let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
   let mty = interp_modtype (Global.env()) arg in
   let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
-  let substobjs = get_modtype_substobjs (Global.env()) mty in
+  let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
+    (MPbound (List.hd mbids))  mty in
   List.map2
     (fun dir mbid ->
-      Global.add_module_parameter mbid mty;
-      let mp = MPbound mbid in
-      ignore (do_load_and_subst_module 1 dir mp substobjs []);
-      (mbid,mty))
+       let resolver = Global.add_module_parameter mbid mty in
+       let mp = MPbound mbid in
+       let substobjs = (mbi,mp,subst_objects 
+			  (map_mp mp_from mp resolver) objs) in
+	 do_module false "interp" load_objects 1 dir mp substobjs [];
+	 (mbid,mty))
     dirs mbids
 
 let start_module interp_modtype export id args res_o =
   let fs = Summary.freeze_summaries () in
-
   let mp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
   let res_entry_o, sub_body_o = match res_o with
       None -> None, None
     | Some (res, restricted) ->
 	(* we translate the module here to catch errors as early as possible *)
 	let mte = interp_modtype (Global.env()) res in
-	if restricted then
-	  Some mte, None
-	else
-	  let mtb,_ = Mod_typing.translate_struct_entry (Global.env()) mte in
-	  let sub_mtb =
-	    List.fold_right
-	      (fun (arg_id,arg_t) mte ->
-		let arg_t,sub = Mod_typing.translate_struct_entry (Global.env()) arg_t
+	  if restricted then
+	    let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in
+	      Some mte, None
+	  else
+	    let mtb = Mod_typing.translate_module_type (Global.env())
+	      mp mte in
+	    let funct_mtb = 
+	      List.fold_right 
+		(fun (arg_id,arg_t) mte -> 
+		let arg_t = Mod_typing.translate_module_type (Global.env())
+		  (MPbound arg_id)  arg_t
 		in
-		let arg_t = {typ_expr = arg_t;
-			     typ_strength = None;
-			     typ_alias = sub} in
 		  SEBfunctor(arg_id,arg_t,mte))
-	      arg_entries mtb
-	  in
-	  None, Some sub_mtb
+		arg_entries mtb.typ_expr
+	    in
+	      None, Some {mtb with 
+			 typ_expr = funct_mtb}
   in
 
   let mbids = List.map fst arg_entries in
-    openmod_info:=(mbids,res_entry_o,sub_body_o);
+    openmod_info:=(mp,mbids,res_entry_o,sub_body_o);
   let prefix = Lib.start_module export id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix);
   Lib.add_frozen_state (); mp
@@ -720,24 +486,25 @@ let start_module interp_modtype export id args res_o =
 let end_module () =
 
   let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
-  let mbids, res_o, sub_o = !openmod_info in
+  let mp,mbids, res_o, sub_o = !openmod_info in
   let substitute, keep, special = Lib.classify_segment lib_stack in
 
-  let dir = fst oldprefix in
-  let msid = msid_of_prefix oldprefix in
-
-  let substobjs, keep, special = try
+  let mp_from,substobjs, keep, special = try
     match res_o with
       | None ->
-	  (empty_subst, mbids, msid, substitute), keep, special
-      | Some (MSEident ln) ->
-	  abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], []
+	  (* the module is not sealed *)
+	  None,( mbids, mp, substitute), keep, special
+      | Some (MSEident ln as mty) ->
+	  let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+	  Some mp1,(mbids@mbids1,mp1,objs), [], []
       | Some (MSEwith _ as mty) ->
-	  abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
+	  let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+	  Some mp1,(mbids@mbids1,mp1,objs), [], []
       | Some (MSEfunctor _) ->
 	  anomaly "Funsig cannot be here..."
       | Some (MSEapply _ as mty) ->
-	  abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
+	  let (mbids1,mp1,objs) = get_modtype_substobjs (Global.env()) mp mty in
+	  Some mp1,(mbids@mbids1,mp1,objs), [], []
   with
 	Not_found -> anomaly "Module objects not found..."
   in
@@ -745,15 +512,21 @@ let end_module () =
      dependencies on functor arguments *)
 
   let id = basename (fst oldoname) in
-  let mp = Global.end_module fs id res_o in
+  let mp,resolver = Global.end_module fs id res_o in
 
   begin match sub_o with
       None -> ()
     | Some sub_mtb -> check_subtypes mp sub_mtb
   end;
 
-  let substituted = subst_substobjs dir mp substobjs in
-  let node = in_module (None,substobjs,substituted) in
+(* we substitute objects if the module is 
+   sealed by a signature (ie. mp_from != None *)
+  let substobjs = match mp_from,substobjs with
+      None,_ -> substobjs
+    | Some mp_from,(mbids,_,objs) ->
+	(mbids,mp,subst_objects (map_mp mp_from mp resolver) objs) 
+  in
+  let node = in_module (None,substobjs) in
   let objects =
     if keep = [] || mbids <> [] then
       special@[node]   (* no keep objects or we are defining a functor *)
@@ -785,28 +558,30 @@ type library_name = dir_path
 
 (* The first two will form substitutive_objects, the last one is keep *)
 type library_objects =
-    mod_self_id * lib_objects * lib_objects
+    module_path * lib_objects * lib_objects
 
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
-  try
+  let substobjs, keep =
+  try 
     ignore(Global.lookup_module mp);
     (* if it's in the environment, the cached objects should be correct *)
-    let substobjs, objects = Dirmap.find dir !library_cache in
-    do_module false "register_library" load_objects 1 dir mp substobjs objects
+    Dirmap.find dir !library_cache
   with Not_found ->
     if mp <> Global.import cenv digest then
       anomaly "Unexpected disk module name";
-    let msid,substitute,keep = objs in
-    let substobjs = empty_subst, [], msid, substitute in
-    let objects = do_load_and_subst_module 1 dir mp substobjs keep in
-    let modobjs = substobjs, objects in
-    library_cache := Dirmap.add dir modobjs !library_cache
+    let mp,substitute,keep = objs in
+    let substobjs = [], mp, substitute in
+    let modobjs = substobjs, keep in
+    library_cache := Dirmap.add dir modobjs !library_cache;
+      modobjs
+  in
+    do_module false "register_library" load_objects 1 dir mp substobjs keep
 
 let start_library dir =
   let mp = Global.start_library dir in
-  openmod_info:=[],None,None;
+  openmod_info:=mp,[],None,None;
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
@@ -816,10 +591,9 @@ let set_end_library_hook f = end_library_hook := f
 let end_library dir =
   !end_library_hook();
   let prefix, lib_stack = Lib.end_compilation dir in
-  let cenv = Global.export dir in
-  let msid = msid_of_prefix prefix in
+  let mp,cenv = Global.export dir in
   let substitute, keep, _ = Lib.classify_segment lib_stack in
-    cenv,(msid,substitute,keep)
+    cenv,(mp,substitute,keep)
 
 
 (* implementation of Export M and Import M *)
@@ -838,8 +612,8 @@ let cache_import (_,(_,mp)) =
 let classify_import (export,_ as obj) =
   if export then Substitute obj else Dispose
 
-let subst_import (_,subst,(export,mp as obj)) =
-  let mp' = subst_mp subst mp in
+let subst_import (subst,(export,mp as obj)) =
+   let mp' = subst_mp subst mp in
     if mp'==mp then obj else
       (export,mp')
 
@@ -870,27 +644,23 @@ let start_modtype interp_modtype id args =
 
 
 let end_modtype () =
-
   let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in
   let id = basename (fst oldoname) in
   let substitute, _, special = Lib.classify_segment lib_stack in
-
-  let msid = msid_of_prefix prefix in
   let mbids = !openmodtype_info in
-  let modtypeobjs = empty_subst, mbids, msid, substitute in
-
-  let ln = Global.end_modtype fs id in
+  let mp = Global.end_modtype fs id in
+  let modtypeobjs = mbids, mp, substitute in  
   let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in
 
   if fst oname <> fst oldoname then
     anomaly
       "Section paths generated on start_ and end_modtype do not match";
-  if (mp_of_kn (snd oname)) <> ln then
+  if (mp_of_kn (snd oname)) <> mp then
     anomaly
       "Kernel and Library names do not match";
 
   Lib.add_frozen_state ()(* to prevent recaching *);
-  ln
+  mp
 
 
 let declare_modtype interp_modtype id args mty =
@@ -907,64 +677,79 @@ let declare_modtype interp_modtype id args mty =
       arg_entries
       base_mty
   in
-  let substobjs = get_modtype_substobjs (Global.env()) entry in
-  (* Undo the simulated interactive building of the module type *)
-  (* and declare the module type as a whole *)
-  Summary.unfreeze_summaries fs;
+  let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp entry in
+    (* Undo the simulated interactive building of the module type *)
+    (* and declare the module type as a whole *)
 
-  ignore (add_leaf id (in_modtype (Some entry, substobjs)));
-  mmp
+  let substobjs = (mbids,mmp,
+		   subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) in
+    Summary.unfreeze_summaries fs;
+    ignore (add_leaf id (in_modtype (Some entry, substobjs)));
+    mmp
   with e ->
     (* Something wrong: undo the whole process *)
     Summary.unfreeze_summaries fs; raise e
 
+(* Small function to avoid module typing during substobjs retrivial  *)
+let rec get_objs_module_application env = function
+| MSEident mp -> 
+    MPmap.find mp !modtab_substobjs,Environ.lookup_module mp env,[]
+| MSEapply (fexpr, MSEident mp) -> 
+    let objs,mtb,mp_l= get_objs_module_application env fexpr in
+      objs,mtb,mp::mp_l
+| MSEapply (_,mexpr) ->
+    Modops.error_application_to_not_path mexpr
+| _ -> error "Application of a non-functor."
 
-let rec get_module_substobjs env = function
+
+let rec get_module_substobjs env mp_from = function
   | MSEident mp -> MPmap.find mp !modtab_substobjs
   | MSEfunctor (mbid,mty,mexpr) ->
-       let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
-	(subst, mbid::mbids, msid, objs)
-  | MSEapply (mexpr, MSEident mp) ->
-      let ftb,sub1 = Mod_typing.translate_struct_entry env mexpr in
-      let farg_id, farg_b, fbody_b = Modops.destr_functor env
-	(Modops.eval_struct env ftb) in
-      let mp = Environ.scrape_alias mp env in
-      let sub_alias = (Environ.lookup_modtype mp env).typ_alias in
-      let sub_alias = match Modops.eval_struct env (SEBident mp) with
-	| SEBstruct (msid,sign) -> join_alias
-	    (subst_key (map_msid msid mp) sub_alias)
-	      (map_msid msid mp)
-	| _ -> sub_alias in
-      let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
+       let (mbids, mp, objs) = get_module_substobjs env mp_from mexpr in
+	(mbid::mbids, mp, objs)
+  | MSEapply (fexpr, MSEident mp) ->
+      let (mbids, mp1, objs),mb_mp1,mp_l =  
+	get_objs_module_application env (MSEapply(fexpr, MSEident mp)) in
+      let rec compute_subst mbids sign mp_l =
+	match mbids,mp_l with
+	    [],[] -> [],empty_subst
+	  | mbid,[] -> mbid,empty_subst
+	  | [],r -> error ("Application of a functor with too few arguments.")
+	  | mbid::mbids,mp::mp_l ->
+	      let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+	      let mb = Environ.lookup_module mp env in
+	      let mp_delta = discr_resolver mb in
+	      let mbid_left,subst=compute_subst mbids fbody_b mp_l in
+		if mp_delta = None then
+		  mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst 
+		else
+		  let mp_delta = Modops.complete_inline_delta_resolver env mp 
+		    farg_id farg_b (Option.get mp_delta) in
+		    mbid_left,join (map_mbid mbid mp mp_delta) subst
+      in
+      let mbids_left,subst = compute_subst mbids mb_mp1.mod_type (List.rev mp_l) in
+	(mbids_left, mp1,subst_objects subst objs)
+    (*  let sign,alg,equiv,_ = Mod_typing.translate_struct_module_entry env mp_from fexpr in
+      let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+      let mb = Environ.lookup_module mp env in
+      let mp_delta = discr_resolver mb in
+      let (mbids, mp1, objs) = get_module_substobjs env mp_from fexpr in
 	(match mbids with
 	   | mbid::mbids ->
-               let resolve =
-		 Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
-	       let sub3=
-		 if sub1 = empty_subst then
-		   update_subst sub_alias (map_mbid farg_id mp None)
-		 else
-		   let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
-		   let sub_alias' =  update_subst sub_alias sub1' in
-		     join sub1' sub_alias'
-	       in
-	       let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
-		 (* application outside the kernel, only for substitutive
-                    objects (that are all non-logical objects) *)
-		((join
-		    (join subst sub3)
-		       (map_mbid mbid mp (Some resolve)))
-		       , mbids, msid, objs)
-	   | [] -> match mexpr with
+	       if mp_delta = None then
+		 (mbids, mp1,subst_objects (map_mbid mbid mp empty_delta_resolver) objs)
+	       else
+		 let mp_delta = Modops.complete_inline_delta_resolver env mp 
+		   farg_id farg_b (Option.get mp_delta) in
+		    (mbids, mp1,subst_objects (map_mbid mbid mp mp_delta) objs)
+	   | [] -> match fexpr with
 	       | MSEident _  -> error "Application of a non-functor."
-	       | _ -> error "Application of a functor with too few arguments.")
+	       | _ -> error "Application of a functor with too few arguments.")*)
   | MSEapply (_,mexpr) ->
       Modops.error_application_to_not_path mexpr
-  | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty
-  | MSEwith (mty, With_Module (idl,mp)) ->
-      let substobjs = get_module_substobjs env mty in
-      let modobjs = MPmap.find mp !modtab_substobjs in
-	replace_module_object idl substobjs modobjs mp
+  | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from mty
+  | MSEwith (mty, With_Module (idl,mp)) -> assert false
+
 
 
 (* Include *)
@@ -991,46 +776,32 @@ let lift_oname (sp,kn) =
   let dir,_ = Libnames.repr_path sp in
     (dir,mp)
 
-let cache_include (oname,((me,is_mod),substobjs,substituted)) =
+let cache_include (oname,((me,is_mod),(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
-    Global.add_include me;
-    match substituted with
-	Some seg ->
-	  load_objects 1 prefix seg;
-	  open_objects 1 prefix seg;
-      | None ->  ()
-
-let load_include  i (oname,((me,is_mod),substobjs,substituted)) =
+    load_objects 1 prefix objs;
+    open_objects 1 prefix objs 
+    
+let load_include  i (oname,((me,is_mod),(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
-    match substituted with
-	Some seg ->
-	  load_objects i prefix seg
-      | None ->  ()
-
-let open_include i (oname,((me,is_mod),substobjs,substituted)) =
+    load_objects i prefix objs
+      
+      
+let open_include i (oname,((me,is_mod),(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
   let prefix = (dir,(mp1,empty_dirpath)) in
-    match substituted with
-	Some seg ->
-	  if is_mod then
-	  open_objects i prefix seg
-	  else
-	    if i = 1 then
-	      open_objects i prefix seg
-      | None ->  ()
-
-let subst_include (oname,subst,((me,is_mod),substobj,_)) =
-  let dir,mp1 = lift_oname oname in
-  let (sub,mbids,msid,objs) = substobj in
-  let subst' = join sub subst in
-  let substobjs = (subst',mbids,msid,objs) in
-  let substituted = subst_substobjs dir mp1 substobjs in
-    ((subst_inc_expr subst' me,is_mod),substobjs,substituted)
-
-let classify_include ((me,is_mod),substobjs,_) =
-  Substitute ((me,is_mod),substobjs,None)
+      if is_mod || i = 1 then
+	open_objects i prefix objs
+      else ()
+    
+let subst_include (subst,((me,is_mod),substobj)) =
+  let (mbids,mp,objs) = substobj in
+  let substobjs = (mbids,subst_mp subst mp,subst_objects subst objs) in
+    ((subst_inc_expr subst me,is_mod),substobjs)
+      
+let classify_include ((me,is_mod),substobjs) =
+  Substitute ((me,is_mod),substobjs)
 
 let (in_include,out_include) =
   declare_object {(default_object "INCLUDE") with
@@ -1040,20 +811,19 @@ let (in_include,out_include) =
     subst_function = subst_include;
     classify_function = classify_include }
 
-let rec update_include (sub,mbids,msid,objs) =
+let rec update_include (mbids,mp,objs) =
   let rec replace_include = function
     | [] -> []
     | (id,obj)::tail ->
 	if object_tag obj = "INCLUDE" then
-	  let ((me,is_mod),substobjs,substituted) = out_include obj in
+	  let ((me,is_mod),substobjs) = out_include obj in
 	  let substobjs' = update_include substobjs in
-            (id, in_include ((me,true),substobjs',substituted))::
+            (id, in_include ((me,true),substobjs'))::
 	      (replace_include tail)
 	else
 	  (id,obj)::(replace_include tail)
   in
-    (sub,mbids,msid,replace_include objs)
-
+    (mbids,mp,replace_include objs)
 
 let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 
@@ -1084,8 +854,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
 	Some (List.fold_right
 		(fun (mbid,mte) me -> MSEfunctor(mbid,mte,me))
 		arg_entries
-		(interp_modexpr (Global.env()) mexpr))
-  in
+		(interp_modexpr (Global.env()) mexpr))  in
   let entry =
     {mod_entry_type = mty_entry_o;
      mod_entry_expr = mexpr_entry_o }
@@ -1093,45 +862,33 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
   let env = Global.env() in
   let substobjs =
     match entry with
-      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mte
-      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr
+      | {mod_entry_type = Some mte} -> get_modtype_substobjs env mmp mte
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp mexpr
       | _ -> anomaly "declare_module: No type, no body ..."
   in
-  let substobjs = update_include substobjs in
+  let (mbids,mp_from,objs) = update_include substobjs in
     (* Undo the simulated interactive building of the module *)
     (* and declare the module as a whole *)
     Summary.unfreeze_summaries fs;
-    match entry with
-      |{mod_entry_type = None;
-	mod_entry_expr = Some (MSEident mp) } ->
-	 let dir,mp' = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
-	 let (sub,mbids,msid,objs) = substobjs in
-	 let mp1 = Environ.scrape_alias mp env in
-	 let prefix =  dir,(mp1,empty_dirpath) in
-	 let substituted =
-	   match mbids with
-		    | [] ->
-			Some (subst_objects prefix
-				(join sub (join (map_msid msid mp1) (map_mp mp' mp1))) objs)
-		    | _ -> None in
-	   ignore (add_leaf
-		     id
-		     (in_module_alias (Some ({mod_entry_type = None;
-					      mod_entry_expr = Some (MSEident mp1) }, mty_sub_o),
-				       substobjs, substituted)));
-	   mmp
-      | _ ->
-	  let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
-	  let (sub,mbids,msid,objs) = substobjs in
-	  let sub' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in
-	  let substobjs = ( sub',mbids,msid,objs) in
-	  let substituted = subst_substobjs dir mp substobjs in
-	    ignore (add_leaf
-		      id
-		      (in_module (Some (entry, mty_sub_o), substobjs, substituted)));
-	    mmp
-
-  with e ->
+    let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
+    let mp_env,resolver = Global.add_module id entry in
+    let _ = if mp_env <> mp then
+      anomaly "Kernel and Library names do not match";
+      match  mty_sub_o with
+	| None -> ()
+	| Some sub_mte -> 
+	    let sub_mtb = Mod_typing.translate_module_type
+	      env mp sub_mte in
+	      check_subtypes mp_env sub_mtb
+    in
+    let substobjs = (mbids,mp_env,
+		     subst_objects(map_mp mp_from mp_env resolver) objs) in
+      ignore (add_leaf
+		id
+		(in_module (Some (entry, mty_sub_o), substobjs)));
+      mmp
+	
+  with e -> 
     (* Something wrong: undo the whole process *)
     Summary.unfreeze_summaries fs; raise e
 
@@ -1142,19 +899,19 @@ let declare_include interp_struct me_ast is_mod =
 
     try
       let env = Global.env() in
-      let me = interp_struct env me_ast in
-      let substobjs =
+      let me = interp_struct env me_ast in 
+      let mp1,_ = current_prefix () in
+      let (mbids,mp,objs)= 	
 	if is_mod then
-	  get_module_substobjs env me
+	  get_module_substobjs env mp1 me
 	else
-	  get_modtype_substobjs env me in
-      let mp1,_ = current_prefix () in
-      let dir = dir_of_sp (Lib.path_of_include()) in
-      let substituted = subst_substobjs dir mp1 substobjs in
+	  get_modtype_substobjs env mp1 me in
       let id = current_mod_id() in
-
+      let resolver =  Global.add_include me is_mod in
+      let substobjs = (mbids,mp1,
+		       subst_objects (map_mp mp mp1 resolver) objs) in
 	ignore (add_leaf id
-		  (in_include ((me,is_mod), substobjs, substituted)))
+		  (in_include ((me,is_mod), substobjs)))
     with e ->
       (* Something wrong: undo the whole process *)
       Summary.unfreeze_summaries fs; raise e
diff --git a/library/global.ml b/library/global.ml
index e228de23a..6d7942ec0 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -48,14 +48,6 @@ let push_named_def d =
   global_env := env;
   cst
 
-(*let add_thing add kn thing =
-  let _,dir,l = repr_kn kn in
-  let kn',newenv = add dir l thing !global_env in
-    if kn = kn' then
-      global_env := newenv
-    else
-      anomaly "Kernel names do not match."
-*)
 
 let add_thing add dir id thing =
   let kn, newenv = add dir (label_of_id id) thing !global_env in
@@ -65,14 +57,23 @@ let add_thing add dir id thing =
 let add_constant = add_thing add_constant
 let add_mind = add_thing add_mind
 let add_modtype = add_thing (fun _ -> add_modtype) ()
-let add_module = add_thing (fun _ -> add_module) ()
-let add_alias = add_thing (fun _ -> add_alias) ()
+
+
+let add_module id me =
+  let l = label_of_id id in
+  let mp,resolve,new_env = add_module l me !global_env in
+    global_env := new_env;
+    mp,resolve
+    
 
 let add_constraints c = global_env := add_constraints c !global_env
 
 let set_engagement c = global_env := set_engagement c !global_env
 
-let add_include me = global_env := add_include me !global_env
+let add_include me is_module =
+  let resolve,newenv = add_include me is_module !global_env in
+    global_env := newenv;
+    resolve
 
 let start_module id =
   let l = label_of_id id in
@@ -82,15 +83,16 @@ let start_module id =
 
 let end_module fs id mtyo =
   let l = label_of_id id in
-  let mp,newenv = end_module l mtyo !global_env in
+  let mp,resolve,newenv = end_module l mtyo !global_env in
     Summary.unfreeze_summaries fs;
     global_env := newenv;
-    mp
+    mp,resolve
 
 
 let add_module_parameter mbid mte =
-  let newenv = add_module_parameter mbid mte !global_env in
-    global_env := newenv
+  let resolve,newenv = add_module_parameter mbid mte !global_env in
+    global_env := newenv;
+    resolve
 
 
 let start_modtype id =
@@ -117,15 +119,22 @@ let lookup_mind kn = lookup_mind kn (env())
 let lookup_module mp = lookup_module mp (env())
 let lookup_modtype kn = lookup_modtype kn (env())
 
+let constant_of_delta con = 
+  let resolver,resolver_param = (delta_of_senv !global_env) in
+    Mod_subst.constant_of_delta resolver_param
+      (Mod_subst.constant_of_delta resolver con)
 
-
-
+let mind_of_delta mind = 
+  let resolver,resolver_param = (delta_of_senv !global_env) in
+    Mod_subst.mind_of_delta resolver_param
+      (Mod_subst.mind_of_delta resolver mind)
+	
 let start_library dir =
   let mp,newenv = start_library dir !global_env in
     global_env := newenv;
     mp
 
-let export s = snd (export !global_env s)
+let export s = export !global_env s
 
 let import cenv digest =
   let mp,newenv = import cenv digest !global_env in
@@ -161,3 +170,5 @@ let register field value by_clause =
   let entry = kind_of_term value in
   let senv = Safe_typing.register !global_env field entry by_clause in
   global_env := senv
+
+
diff --git a/library/global.mli b/library/global.mli
index 3c2317122..30bd04150 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -15,6 +15,7 @@ open Term
 open Declarations
 open Entries
 open Indtypes
+open Mod_subst
 open Safe_typing
    (*i*)
 
@@ -47,12 +48,11 @@ val push_named_def   : (identifier * constr * types option) -> Univ.constraints
 val add_constant :
   dir_path -> identifier -> global_declaration -> constant
 val add_mind        :
-  dir_path -> identifier -> mutual_inductive_entry -> kernel_name
+  dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive
 
-val add_module      : identifier -> module_entry -> module_path
+val add_module      : identifier -> module_entry -> module_path * delta_resolver
 val add_modtype     : identifier -> module_struct_entry -> module_path
-val add_include : module_struct_entry -> unit
-val add_alias : identifier -> module_path -> module_path
+val add_include : module_struct_entry -> bool -> delta_resolver
 
 val add_constraints : constraints -> unit
 
@@ -66,10 +66,11 @@ val set_engagement : engagement -> unit
    of the started module / module type *)
 
 val start_module : identifier -> module_path
-val end_module :
-  Summary.frozen -> identifier -> module_struct_entry option -> module_path
 
-val add_module_parameter : mod_bound_id -> module_struct_entry -> unit
+val end_module : Summary.frozen ->identifier -> module_struct_entry option -> 
+  module_path * delta_resolver
+
+val add_module_parameter : mod_bound_id -> module_struct_entry -> delta_resolver
 
 val start_modtype : identifier -> module_path
 val end_modtype : Summary.frozen -> identifier -> module_path
@@ -83,10 +84,12 @@ val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body
 val lookup_mind      : mutual_inductive -> mutual_inductive_body
 val lookup_module    : module_path -> module_body
 val lookup_modtype   : module_path -> module_type_body
+val constant_of_delta : constant -> constant
+val mind_of_delta : mutual_inductive -> mutual_inductive
 
 (* Compiled modules *)
 val start_library : dir_path -> module_path
-val export : dir_path -> compiled_library
+val export : dir_path -> module_path * compiled_library
 val import : compiled_library -> Digest.t -> module_path
 
 (*s Function to get an environment from the constants part of the global
diff --git a/library/goptions.ml b/library/goptions.ml
index 032016c3d..06d4b618e 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -91,7 +91,7 @@ module MakeTable =
           | GOadd -> t := MySet.add p !t
           | GOrmv -> t := MySet.remove p !t in
         let load_options i o = if i=1 then cache_options o in
-	let subst_options (_,subst,(f,p as obj)) =
+	let subst_options (subst,(f,p as obj)) = 
 	  let p' = A.subst subst p in
 	    if p' == p then obj else
 	      (f,p')
diff --git a/library/heads.ml b/library/heads.ml
index 150ba8942..056f78a5f 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -39,8 +39,20 @@ type head_approximation =
 
 (** Registration as global tables and rollback. *)
 
+module Evalreford = struct
+  type t = evaluable_global_reference
+  let compare x y = 
+     let make_name = function
+      | EvalConstRef con -> 
+	  EvalConstRef(constant_of_kn(canonical_con con))
+      | k -> k
+     in 
+       Pervasives.compare (make_name x) (make_name y)
+end
+
 module Evalrefmap =
-  Map.Make (struct type t = evaluable_global_reference let compare = compare end)
+  Map.Make (Evalreford)
+
 
 let head_map = ref Evalrefmap.empty
 
@@ -144,7 +156,7 @@ let subst_head_approximation subst = function
         kind_of_head (Global.env()) c
   | x -> x
 
-let subst_head (_,subst,(ref,k)) =
+let subst_head (subst,(ref,k)) =
   (subst_evaluable_reference subst ref, subst_head_approximation subst k)
 
 let discharge_head (_,(ref,k)) =
diff --git a/library/impargs.ml b/library/impargs.ml
index d27ced220..1edac69aa 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -435,7 +435,7 @@ type implicit_interactive_request =
 type implicit_discharge_request =
   | ImplLocal
   | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of kernel_name * implicits_flags
+  | ImplMutualInductive of mutual_inductive * implicits_flags
   | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
@@ -455,7 +455,7 @@ let cache_implicits o =
 let subst_implicits_decl subst (r,imps as o) =
   let r' = fst (subst_global subst r) in if r==r' then o else (r',imps)
 
-let subst_implicits (_,subst,(req,l)) =
+let subst_implicits (subst,(req,l)) =
   (ImplLocal,list_smartmap (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
diff --git a/library/impargs.mli b/library/impargs.mli
index 6d2b01e8f..e8191e863 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -108,7 +108,7 @@ type implicit_interactive_request =
 type implicit_discharge_request =
   | ImplLocal
   | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of kernel_name * implicits_flags
+  | ImplMutualInductive of mutual_inductive * implicits_flags
   | ImplInteractive of global_reference * implicits_flags *
       implicit_interactive_request
 
diff --git a/library/lib.ml b/library/lib.ml
index 961a4ebb9..b8dcee9d2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -37,21 +37,21 @@ let iter_objects f i prefix =
 let load_objects = iter_objects load_object
 let open_objects = iter_objects open_object
 
-let subst_objects prefix subst seg =
+let subst_objects subst seg = 
   let subst_one = fun (id,obj as node) ->
-    let obj' = subst_object (make_oname prefix id, subst, obj) in
+    let obj' = subst_object (subst,obj) in
       if obj' == obj then node else
 	(id, obj')
   in
     list_smartmap subst_one seg
 
-let load_and_subst_objects i prefix subst seg =
+(*let load_and_subst_objects i prefix subst seg =
   List.rev (List.fold_left (fun seg (id,obj as node) ->
     let obj' =  subst_object (make_oname prefix id, subst, obj) in
     let node = if obj == obj' then node else (id, obj') in
     load_object i (make_oname prefix id, obj');
     node :: seg) [] seg)
-
+*)
 let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
@@ -435,13 +435,13 @@ type binding_kind = Explicit | Implicit
 
 type variable_info = Names.identifier * binding_kind * Term.constr option * Term.types
 type variable_context = variable_info list
-type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
+type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t
 
 let sectab =
   ref ([] : ((Names.identifier * binding_kind) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
-  sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
+  sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty),(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
 let add_section_variable id impl =
   match !sectab with
@@ -474,7 +474,7 @@ let add_section_replacement f g hyps =
     sectab := (vars,f args exps,g sechyps abs)::sl
 
 let add_section_kn kn =
-  let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in
+  let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
   add_section_replacement f f
 
 let add_section_constant kn =
@@ -489,7 +489,7 @@ let section_segment_of_constant con =
   Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
 
 let section_segment_of_mutual_inductive kn =
-  Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
+  Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
 
 let rec list_mem_assoc x = function
   | [] -> raise Not_found
@@ -502,7 +502,7 @@ let section_instance = function
   | ConstRef con ->
       Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
   | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
-      Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
+      Names.Mindmap.find kn (snd (pi2 (List.hd !sectab)))
 
 let is_in_section ref =
   try ignore (section_instance ref); true with Not_found -> false
@@ -772,7 +772,7 @@ let mp_of_global ref =
 let rec dp_of_mp modp =
   match modp with
     | Names.MPfile dp -> dp
-    | Names.MPbound _ | Names.MPself _ -> library_dp ()
+    | Names.MPbound _ -> library_dp ()
     | Names.MPdot (mp,_) -> dp_of_mp mp
 
 let rec split_mp mp =
@@ -781,7 +781,6 @@ let rec split_mp mp =
     | Names.MPdot (prfx, lbl) ->
 	let mprec, dprec = split_mp prfx in
 	  mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
-    | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
     | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [Names.id_of_string id]
 
 let split_modpath mp =
@@ -789,7 +788,6 @@ let split_modpath mp =
     | Names.MPfile dp -> dp, []
     | Names.MPbound mbid ->
 	library_dp (), [Names.id_of_mbid mbid]
-    | Names.MPself msid -> library_dp (), [Names.id_of_msid msid]
     | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
 			      (mp', Names.id_of_label l :: lab)
   in
@@ -819,8 +817,8 @@ let remove_section_part ref =
 (* Discharging names *)
 
 let pop_kn kn =
-  let (mp,dir,l) = Names.repr_kn kn in
-  Names.make_kn mp (pop_dirpath dir) l
+  let (mp,dir,l) = Names.repr_mind kn in
+  Names.make_mind mp (pop_dirpath dir) l
 
 let pop_con con =
   let (mp,dir,l) = Names.repr_con con in
@@ -831,7 +829,7 @@ let con_defined_in_sec kn =
   dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
 
 let defined_in_sec kn =
-  let _,dir,_ = Names.repr_kn kn in
+  let _,dir,_ = Names.repr_mind kn in
   dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
 
 let discharge_global = function
diff --git a/library/lib.mli b/library/lib.mli
index 0e2e304cd..32d1c0009 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -32,8 +32,8 @@ type lib_objects = (Names.identifier * Libobject.obj) list
 
 val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
 val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
-val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
-val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
+val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects
+(*val load_and_subst_objects : int -> Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects*)
 
 (* [classify_segment seg] verifies that there are no OpenedThings,
    clears ClosedSections and FrozenStates and divides Leafs according
@@ -183,13 +183,13 @@ val is_in_section : Libnames.global_reference -> bool
 val add_section_variable : Names.identifier -> binding_kind -> unit
 
 val add_section_constant : Names.constant -> Sign.named_context -> unit
-val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
+val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit
 val replacement_context : unit ->
-  (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t)
+  (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t)
 
 (*s Discharge: decrease the section level if in the current section *)
 
-val discharge_kn :  Names.kernel_name -> Names.kernel_name
+val discharge_kn :  Names.mutual_inductive -> Names.mutual_inductive
 val discharge_con : Names.constant -> Names.constant
 val discharge_global : Libnames.global_reference -> Libnames.global_reference
 val discharge_inductive : Names.inductive -> Names.inductive
diff --git a/library/libnames.ml b/library/libnames.ml
index 2b335ea6c..fad0336fc 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -27,13 +27,21 @@ let isConstRef = function ConstRef _ -> true | _ -> false
 let isIndRef = function IndRef _ -> true | _ -> false
 let isConstructRef = function ConstructRef _ -> true | _ -> false
 
+let eq_gr gr1 gr2 =
+  match gr1,gr2 with 
+      ConstRef con1, ConstRef con2 ->
+	eq_constant con1 con2
+    | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2
+    | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2
+    | _,_ -> gr1=gr2
+
 let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
 let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
 
 let subst_constructor subst ((kn,i),j as ref) =
-  let kn' = subst_kn subst kn in
+  let kn' = subst_ind subst kn in
     if kn==kn' then ref, mkConstruct ref
     else ((kn',i),j), mkConstruct ((kn',i),j)
 
@@ -43,7 +51,7 @@ let subst_global subst ref = match ref with
      let kn',t = subst_con subst kn in
       if kn==kn' then ref, mkConst kn else ConstRef kn', t
   | IndRef (kn,i) ->
-      let kn' = subst_kn subst kn in
+      let kn' = subst_ind subst kn in
       if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
   | ConstructRef ((kn,i),j as c) ->
       let c',t = subst_constructor subst c in
@@ -65,15 +73,25 @@ let constr_of_global = function
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
-module RefOrdered =
-  struct
-    type t = global_reference
-    let compare = Pervasives.compare
-  end
-
+(* outside of the kernel, names are ordered on their canonical part *)
+module RefOrdered = struct
+  type t = global_reference
+  let compare x y = 
+    let make_name = function
+      | ConstRef con -> 
+	  ConstRef(constant_of_kn(canonical_con con))
+      | IndRef (kn,i) ->
+	  IndRef(mind_of_kn(canonical_mind kn),i)
+      | ConstructRef ((kn,i),j )->
+	  ConstructRef((mind_of_kn(canonical_mind kn),i),j)
+      | VarRef id ->  VarRef id
+    in
+	Pervasives.compare (make_name x) (make_name y)
+end
+  
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
-
+  
 (* Extended global references *)
 
 type syndef_name = kernel_name
@@ -191,26 +209,22 @@ let restrict_path n sp =
   let dir' = list_firstn n (repr_dirpath dir) in
   make_path (make_dirpath dir') s
 
-let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
+let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id)
 
 let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
 
-let decode_kn kn =
-  let rec dirpath_of_module = function
+let decode_mind kn =
+  let rec dir_of_mp = function
     | MPfile dir -> repr_dirpath dir
-    | MPbound mbid ->
+    | MPbound mbid -> 
 	let _,_,dp = repr_mbid mbid in
 	let id = id_of_mbid mbid in
 	  id::(repr_dirpath dp)
-    | MPself msid ->
-	let _,_,dp = repr_msid msid in
-	let id = id_of_msid msid in
-	  id::(repr_dirpath dp)
-    | MPdot(mp,l) -> (id_of_label l)::(dirpath_of_module mp)
+    | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
   in
-  let mp,sec_dir,l = repr_kn kn in
+  let mp,sec_dir,l = repr_mind kn in
     if (repr_dirpath sec_dir) = [] then
-     (make_dirpath (dirpath_of_module mp)),id_of_label l
+     (make_dirpath (dir_of_mp mp)),id_of_label l
     else
       anomaly "Section part should be empty!"
 
@@ -289,8 +303,8 @@ let pop_con con =
   Names.make_con mp (pop_dirpath dir) l
 
 let pop_kn kn =
-  let (mp,dir,l) = repr_kn kn in
-  Names.make_kn mp (pop_dirpath dir) l
+  let (mp,dir,l) = repr_mind kn in
+  Names.make_mind mp (pop_dirpath dir) l
 
 let pop_global_reference = function
   | ConstRef con -> ConstRef (pop_con con)
diff --git a/library/libnames.mli b/library/libnames.mli
index 43ca252c1..fd2ca37ae 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -28,11 +28,14 @@ val isConstRef : global_reference -> bool
 val isIndRef : global_reference -> bool
 val isConstructRef : global_reference -> bool
 
+val eq_gr : global_reference -> global_reference -> bool
+
 val destVarRef : global_reference -> variable
 val destConstRef : global_reference -> constant
 val destIndRef : global_reference -> inductive
 val destConstructRef : global_reference -> constructor
 
+
 val subst_constructor : substitution -> constructor -> constructor * constr
 val subst_global : substitution -> global_reference -> global_reference * constr
 
@@ -47,6 +50,12 @@ val global_of_constr : constr -> global_reference
 val constr_of_reference : global_reference -> constr
 val reference_of_constr : constr -> global_reference
 
+module RefOrdered : sig
+  type t = global_reference
+  val compare : global_reference -> global_reference -> int
+end
+  
+
 module Refset : Set.S with type elt = global_reference
 module Refmap : Map.S with type key = global_reference
 
@@ -108,8 +117,8 @@ val restrict_path : int -> full_path -> full_path
 
 (*s Temporary function to brutally form kernel names from section paths *)
 
-val encode_kn : dir_path -> identifier -> kernel_name
-val decode_kn : kernel_name -> dir_path * identifier
+val encode_mind : dir_path -> identifier -> mutual_inductive
+val decode_mind : mutual_inductive -> dir_path * identifier
 val encode_con : dir_path -> identifier -> constant
 val decode_con : constant -> dir_path * identifier
 
@@ -170,7 +179,7 @@ val loc_of_reference : reference -> loc
 (*s Popping one level of section in global names *)
 
 val pop_con : constant -> constant
-val pop_kn : kernel_name -> kernel_name
+val pop_kn : mutual_inductive-> mutual_inductive
 val pop_global_reference : global_reference -> global_reference
 
 (* Deprecated synonyms *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 4bd701e13..ecdcacf1d 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -34,7 +34,7 @@ type 'a object_declaration = {
   load_function : int -> object_name * 'a -> unit;
   open_function : int -> object_name * 'a -> unit;
   classify_function : 'a -> 'a substitutivity;
-  subst_function : object_name * substitution * 'a -> 'a;
+  subst_function :  substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
@@ -63,7 +63,7 @@ let default_object s = {
    This helps introducing new functions in objects.
 *)
 
-let ident_subst_function (_,_,a) = a
+let ident_subst_function (_,a) = a
 
 type obj = Dyn.t (* persistent dynamic objects *)
 
@@ -71,7 +71,7 @@ type dynamic_object_declaration = {
   dyn_cache_function : object_name * obj -> unit;
   dyn_load_function : int -> object_name * obj -> unit;
   dyn_open_function : int -> object_name * obj -> unit;
-  dyn_subst_function : object_name * substitution * obj -> obj;
+  dyn_subst_function : substitution * obj -> obj;
   dyn_classify_function : obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
   dyn_rebuild_function : obj -> obj }
@@ -93,9 +93,9 @@ let declare_object odecl =
   and opener i (oname,lobj) =
     if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the openfun"
-  and substituter (oname,sub,lobj) =
-    if Dyn.tag lobj = na then
-      infun (odecl.subst_function (oname,sub,outfun lobj))
+  and substituter (sub,lobj) = 
+    if Dyn.tag lobj = na then 
+      infun (odecl.subst_function (sub,outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the substfun"
   and classifier lobj =
     if Dyn.tag lobj = na then
@@ -158,7 +158,7 @@ let load_object i ((_,lobj) as node) =
 let open_object i ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj
 
-let subst_object ((_,_,lobj) as node) =
+let subst_object ((_,lobj) as node) = 
   apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
 
 let classify_object lobj =
diff --git a/library/libobject.mli b/library/libobject.mli
index 834a70c64..9c0abafde 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -70,7 +70,7 @@ type 'a object_declaration = {
   load_function : int -> object_name * 'a -> unit;
   open_function : int -> object_name * 'a -> unit;
   classify_function : 'a -> 'a substitutivity;
-  subst_function : object_name * substitution * 'a -> 'a;
+  subst_function :  substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
   rebuild_function : 'a -> 'a }
 
@@ -86,7 +86,7 @@ type 'a object_declaration = {
 val default_object : string -> 'a object_declaration
 
 (* the identity substitution function *)
-val ident_subst_function : object_name * substitution * 'a -> 'a
+val ident_subst_function : substitution * 'a -> 'a
 
 (*s Given an object declaration, the function [declare_object]
    will hand back two functions, the "injection" and "projection"
@@ -102,7 +102,7 @@ val object_tag : obj -> string
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
 val open_object : int -> object_name * obj -> unit
-val subst_object : object_name * substitution * obj -> obj
+val subst_object : substitution * obj -> obj
 val classify_object : obj -> obj substitutivity
 val discharge_object : object_name * obj -> obj option
 val rebuild_object : obj -> obj
diff --git a/library/library.ml b/library/library.ml
index d129a24db..fbe437fc4 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -302,7 +302,7 @@ let open_import i (_,(dir,export)) =
 let cache_import obj =
   open_import 1 obj
 
-let subst_import (_,_,o) = o
+let subst_import (_,o) = o
 
 let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
diff --git a/library/nametab.ml b/library/nametab.ml
index 31915c95a..c14b6cfc0 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -314,18 +314,26 @@ let the_tacticrevtab = ref (KNmap.empty : knrevtab)
    Parameter but also Remark and Fact) *)
 
 let push_xref visibility sp xref =
-  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
   match visibility with
     | Until _ ->
-	if Globrevtab.mem xref !the_globrevtab then
-	  ()
-	else
-	  the_globrevtab := Globrevtab.add xref sp !the_globrevtab
-    | _ -> ()
+	the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+    | _ ->
+	begin
+	  if SpTab.exists sp !the_ccitab then
+	    match SpTab.find sp !the_ccitab with
+	      | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
+		    TrueGlobal( ConstructRef _) as xref ->
+		  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	      | _ -> 
+		  the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	    else
+	      the_ccitab := SpTab.push visibility sp xref !the_ccitab;
+	end
 
 let push_cci visibility sp ref =
   push_xref visibility sp (TrueGlobal ref)
-
+    
 (* This is for Syntactic Definitions *)
 let push_syndef visibility sp kn =
   push_xref visibility sp (SynDef kn)