Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 544 insertions, 753 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index cfada00c..4449c531 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declaremods.ml 12295 2009-08-27 11:01:49Z soubiran $ i*)
+(*i $Id$ i*)
+
 open Pp
 open Util
 open Names
@@ -21,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).
@@ -39,157 +40,161 @@ open Mod_subst
    therefore must be substitued with valid names before use.
 
 *)
-type substitutive_objects = 
-    substitution * mod_bound_id list * mod_self_id * lib_objects
+type substitutive_objects =
+     mod_bound_id list * module_path * lib_objects
 
 
 (* For each module, we store the following things:
 
-   In modtab_substobjs: substitutive_objects 
-     when we will do Module M:=N, the objects of N will be reloaded 
+   In modtab_substobjs: substitutive_objects
+     when we will do Module M:=N, the objects of N will be reloaded
      with M after substitution
 
    In modtab_objects: "substituted objects" @ "keep objects"
 
-   substituted objects - 
-     roughly the objects above after the substitution - we need to 
+   substituted objects -
+     roughly the objects above after the substitution - we need to
      keep them to call open_object when the module is opened (imported)
- 
+
    keep objects -
-     The list of non-substitutive objects - as above, for each of 
-     them we will call open_object when the module is opened 
-     
+     The list of non-substitutive objects - as above, for each of
+     them we will call open_object when the module is opened
+
    (Some) Invariants:
    * If the module is a functor, the two latter lists are empty.
 
-   * Module objects in substitutive_objects part have empty substituted 
+   * Module objects in substitutive_objects part have empty substituted
      objects.
 
-   * Modules which where created with Module M:=mexpr or with 
+   * Modules which where created with Module M:=mexpr or with
      Module M:SIG. ... End M. have the keep list empty.
 *)
-let modtab_substobjs = 
+let modtab_substobjs =
   ref (MPmap.empty : substitutive_objects MPmap.t)
-let modtab_objects = 
+let modtab_objects =
   ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)
 
 
 (* 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,[])
+	 : module_path *  mod_bound_id list *
+           (module_struct_entry * bool) option * module_type_body list)
 
 (* The library_cache here is needed to avoid recalculations of
    substituted modules object during "reloading" of libraries *)
 let library_cache = ref Dirmap.empty
 
 let _ = Summary.declare_summary "MODULE-INFO"
-	  { Summary.freeze_function = (fun () -> 
+	  { Summary.freeze_function = (fun () ->
 					 !modtab_substobjs,
 					 !modtab_objects,
 					 !openmod_info,
 					 !library_cache);
-	    Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) -> 
+	    Summary.unfreeze_function = (fun (sobjs,objs,info,libcache) ->
 					   modtab_substobjs := sobjs;
 					   modtab_objects := objs;
 					   openmod_info := info;
 					   library_cache := libcache);
-	    Summary.init_function = (fun () -> 
+	    Summary.init_function = (fun () ->
 				       modtab_substobjs := MPmap.empty;
 				       modtab_objects := MPmap.empty;
-				       openmod_info := ([],None,None);
-				       library_cache := Dirmap.empty);
-	    Summary.survive_module = false;
-	    Summary.survive_section = false }
+				       openmod_info := ((MPfile(initial_dir),
+							 [],None,[]));
+				       library_cache := Dirmap.empty) }
 
-(* auxiliary functions to transform section_path and kernel_name given
+(* auxiliary functions to transform full_path and kernel_name given
    by Lib into module_path and dir_path needed for modules *)
 
-let mp_of_kn kn = 
-  let mp,sec,l = repr_kn kn in 
-    if sec=empty_dirpath then 
-      MPdot (mp,l) 
+let mp_of_kn kn =
+  let mp,sec,l = repr_kn kn in
+    if sec=empty_dirpath then
+      MPdot (mp,l)
     else
       anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
 
-let is_bound mp =
-  match mp with
-    | MPbound _ -> true
-    | _ -> false
-
-let dir_of_sp sp = 
+let dir_of_sp sp =
   let dir,id = repr_path sp in
-    extend_dirpath dir id
+    add_dirpath_suffix dir id
 
-let msid_of_mp = function
-    MPself msid -> msid
-  | _ -> anomaly "'Self' module path expected!"
+(* Subtyping checks *)
 
-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())
-	
+let check_sub mtb sub_mtb_l =
+  (* The constraints are checked and forgot immediately : *)
+  ignore (List.fold_right
+	    (fun sub_mtb env ->
+	       Environ.add_constraints
+		 (Subtyping.check_subtypes env mtb sub_mtb) env)
+	    sub_mtb_l (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) 
-  in
-    ()  (* The constraints are checked and forgot immediately! *) 
+   a subtype of all signatures in [sub_mtb_l]. Uses only the global
+   environment. *)
 
-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 check_subtypes mp sub_mtb_l =
+  let env = Global.env () in
+  let mb = Environ.lookup_module mp env in
+  let mtb = Modops.module_type_of_module env None mb in
+  check_sub mtb sub_mtb_l
+
+(* Same for module type [mp] *)
+
+let check_subtypes_mt mp sub_mtb_l =
+  check_sub (Environ.lookup_modtype mp (Global.env())) sub_mtb_l
+
+(* Create a functor type entry *)
+
+let funct_entry args m =
+  List.fold_right
+    (fun (arg_id,(arg_t,_)) mte -> MSEfunctor (arg_id,arg_t,mte))
+    args m
+
+(* Prepare the module type list for check of subtypes *)
+
+let build_subtypes interp_modtype mp args mtys =
+  List.map
+    (fun (m,inl) ->
+       let mte = interp_modtype (Global.env()) m in
+       let mtb = Mod_typing.translate_module_type (Global.env()) mp inl mte in
+       let funct_mtb =
+	 List.fold_right
+           (fun (arg_id,(arg_t,arg_inl)) mte ->
+              let arg_t =
+		Mod_typing.translate_module_type (Global.env())
+		  (MPbound arg_id) arg_inl arg_t
+	      in
+              SEBfunctor(arg_id,arg_t,mte))
+           args mtb.typ_expr
+       in
+       { mtb with typ_expr = funct_mtb })
+    mtys
 
-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 *)
 
 let compute_visibility exists what i dir dirinfo =
-  if exists then 
-    if 
-      try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo 
-      with Not_found -> false 
+  if exists then
+    if
+      try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo
+      with Not_found -> false
     then
       Nametab.Exactly i
     else
       errorlabstrm (what^"_module")
-	(pr_dirpath dir ++ str " should already exist!") 
+	(pr_dirpath dir ++ str " should already exist!")
   else
     if Nametab.exists_dir dir then
       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
@@ -200,101 +205,63 @@ 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 ->  ()
-
-let conv_names_do_module exists what iter_objects i 
-      (sp,kn) substobjs substituted =
+    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 =
   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 -> ()
-     | Some _ -> 
+     | Some _ ->
 	 anomaly ("We should never have full info in " ^ s^"!")
 
 
 (* 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
@@ -302,182 +269,17 @@ let (in_module,out_module) =
     load_function = load_module;
     open_function = open_module;
     subst_function = subst_module;
-    classify_function = classify_module;
-    export_function = (fun _ -> anomaly "No modules in sections!") }
-
-
-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;  
-		    export_function = (fun _ -> anomaly "No modules in sections!") }
-    
-
-
-
+    classify_function = classify_module }
 
 let cache_keep _ = anomaly "This module should not be cached!"
 
-let load_keep i ((sp,kn),seg) = 
+let load_keep i ((sp,kn),seg) =
   let mp = mp_of_kn kn in
   let prefix = dir_of_sp sp, (mp,empty_dirpath) in
-    begin 
+    begin
       try
 	let prefix',objects = MPmap.find mp !modtab_objects in
-	  if prefix' <> prefix then 
+	  if prefix' <> prefix then
 	    anomaly "Two different modules with the same path!";
 	  modtab_objects := MPmap.add mp (prefix,objects@seg) !modtab_objects;
       with
@@ -485,16 +287,15 @@ let load_keep i ((sp,kn),seg) =
     end;
     load_objects i prefix seg
 
-let open_keep i ((sp,kn),seg) = 
+let open_keep i ((sp,kn),seg) =
   let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
     open_objects i (dirpath,(mp,empty_dirpath)) seg
 
-let (in_modkeep,out_modkeep) = 
+let (in_modkeep,_) =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
     cache_function = cache_keep;
     load_function = load_keep;
-    open_function = open_keep;
-    export_function = (fun _ -> anomaly "No modules in sections!") }
+    open_function = open_keep }
 
 (* we remember objects for a module type. In case of a declaration:
    Module M:SIG:=...
@@ -506,7 +307,7 @@ let modtypetab =
 (* currently started interactive module type. We remember its arguments
    if it is a functor type *)
 let openmodtype_info =
-  ref ([] : mod_bound_id list)
+  ref ([],[] : mod_bound_id list * module_type_body list)
 
 let _ = Summary.declare_summary "MODTYPE-INFO"
 	  { Summary.freeze_function = (fun () ->
@@ -516,261 +317,253 @@ let _ = Summary.declare_summary "MODTYPE-INFO"
 					   openmodtype_info := snd ft);
 	    Summary.init_function = (fun () ->
 				       modtypetab := MPmap.empty;
-				       openmodtype_info := []);
-	    Summary.survive_module = false;
-	    Summary.survive_section = true }
+				       openmodtype_info := [],[]) }
 
 
-let cache_modtype ((sp,kn),(entry,modtypeobjs)) =
-  let _ = 
+let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) =
+  let mp = mp_of_kn kn in
+
+  let _ =
     match entry with
       | None ->
 	  anomaly "You must not recache interactive module types!"
-      | Some mte ->
-	  let mp = Global.add_modtype (basename sp) mte in
-	  if mp <>mp_of_kn kn then
+      | Some (mte,inl) ->
+	  if mp <> Global.add_modtype (basename sp) mte inl then
 	    anomaly "Kernel and Library names do not match"
   in
 
+  (* Using declare_modtype should lead here, where we check
+     that any given subtyping is indeed accurate *)
+  check_subtypes_mt mp sub_mty_l;
+
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
-      (pr_sp sp ++ str " already exists") ;
+      (pr_path sp ++ str " already exists") ;
 
-  Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn);
+  Nametab.push_modtype (Nametab.Until 1) sp mp;
 
-  modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
+  modtypetab := MPmap.add mp modtypeobjs !modtypetab
 
 
-let load_modtype i ((sp,kn),(entry,modtypeobjs)) =
+let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) =
   check_empty "load_modtype" entry;
 
   if Nametab.exists_modtype sp then
     errorlabstrm "cache_modtype"
-      (pr_sp sp ++ str " already exists") ;
+      (pr_path sp ++ str " already exists") ;
 
   Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn);
-    
+
   modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab
 
 
-let open_modtype i ((sp,kn),(entry,_)) =
+let open_modtype i ((sp,kn),(entry,_,_)) =
   check_empty "open_modtype" entry;
 
-  if 
-    try Nametab.locate_modtype (qualid_of_sp sp) <> (mp_of_kn kn) 
+  if
+    try Nametab.locate_modtype (qualid_of_path sp) <> (mp_of_kn kn)
     with Not_found -> true
   then
-    errorlabstrm ("open_modtype") 
-      (pr_sp sp ++ str " should already exist!");
+    errorlabstrm ("open_modtype")
+      (pr_path sp ++ str " should already exist!");
 
   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)) =
-  Substitute (None,substobjs)
+let classify_modtype (_,substobjs,_) =
+  Substitute (None,substobjs,[])
 
 
-let (in_modtype,out_modtype) =
+let (in_modtype,_) =
     declare_object {(default_object "MODULE TYPE") with
       cache_function = cache_modtype;
       open_function = open_modtype;
       load_function = load_modtype;
       subst_function = subst_modtype;
-      classify_function = classify_modtype;
-      export_function = Option.make }
+      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 compute_subst env mbids sign mp_l inline =
+  match mbids,mp_l with
+    | _,[] -> mbids,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 mbid_left,subst = compute_subst env mbids fbody_b mp_l inline in
+	match discr_resolver mb with
+	  | None ->
+	      mbid_left,join (map_mbid mbid mp empty_delta_resolver) subst
+	  | Some mp_delta ->
+	      let mp_delta =
+		if not inline then mp_delta else
+		  Modops.complete_inline_delta_resolver env mp
+		    farg_id farg_b mp_delta
+	      in
+	      mbid_left,join (map_mbid mbid mp mp_delta) subst
+
+let rec get_modtype_substobjs env mp_from inline = 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
-      let mbid,mbids= (match mbids with
-	   | mbid::mbids -> mbid,mbids
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments") in
-      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 (Some resolve))
-	else
-	  let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
-	  let sub_alias' =  update_subst sub_alias sub1' in
-	    join sub1' sub_alias'
+      let (mbids, mp, objs) = get_modtype_substobjs env mp_from inline mte in
+	(mbid::mbids, mp, objs)
+  | MSEwith (mty, With_Definition _) ->
+      get_modtype_substobjs env mp_from inline mty
+  | MSEwith (mty, With_Module (idl,mp1)) -> 
+      let substobjs = get_modtype_substobjs env mp_from inline mty in
+      let modobjs = MPmap.find mp1 !modtab_substobjs in
+	replace_module_object idl substobjs modobjs mp1
+  | MSEapply (fexpr, MSEident mp) as me ->
+      let (mbids, mp1, objs),mtb_mp1,mp_l =
+	get_objs_modtype_application env me in
+      let mbids_left,subst =
+	compute_subst env mbids mtb_mp1.typ_expr (List.rev mp_l) inline
       in
-      let sub3 = join sub3 
-	(update_subst sub_alias (map_mbid farg_id mp (Some resolve))) 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)
+      (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 process_arg id (mbid,(mty,inl)) =
     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 intern_args interp_modtype (idl,arg) = 
+    let (mbids,mp_from,objs) =
+      get_modtype_substobjs (Global.env()) mp inl 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,inl)) =
   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)) inl 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))
+    (fun dir mbid ->
+       let resolver = Global.add_module_parameter mbid mty inl 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,inl)))
     dirs mbids
 
-let start_module interp_modtype export id args res_o =
-  let fs = Summary.freeze_summaries () in
-
+let start_module_ interp_modtype export id args res fs =
   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 res_entry_o, sub_body_l = match res with
+    | Topconstr.Enforce (res,inl) ->
 	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
-		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
+	let _ = Mod_typing.translate_struct_type_entry (Global.env()) inl mte in
+	Some (mte,inl), []
+    | Topconstr.Check resl ->
+	None, build_subtypes interp_modtype mp arg_entries resl
   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_l);
   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
 
 
-let end_module id =
+let end_module () =
 
-  let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
-  let mbids, res_o, sub_o = !openmod_info in
+  let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in
+  let mp,mbids, res_o, sub_l = !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)), [], []
-      | Some (MSEwith _ as mty) ->
-	  abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], []
-      | Some (MSEfunctor _) -> 
+      | None ->
+	  (* the module is not sealed *)
+	  None,( mbids, mp, substitute), keep, special
+      | Some (MSEident ln as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline mty in
+	  Some mp1,(mbids@mbids1,mp1,objs), [], []
+      | Some (MSEwith _ as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline 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), [], []
+      | Some (MSEapply _ as mty, inline) ->
+	  let (mbids1,mp1,objs) =
+	    get_modtype_substobjs (Global.env()) mp inline mty in
+	  Some mp1,(mbids@mbids1,mp1,objs), [], []
   with
 	Not_found -> anomaly "Module objects not found..."
   in
     (* must be called after get_modtype_substobjs, because of possible
      dependencies on functor arguments *)
 
-  let mp = Global.end_module id res_o in
+  let id = basename (fst oldoname) 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;
+  check_subtypes mp sub_l;
 
-  Summary.module_unfreeze_summaries fs;
-
-  let substituted = subst_substobjs dir mp substobjs in
-  let node = in_module (None,substobjs,substituted) in
-  let objects = 
-    if keep = [] || mbids <> [] then 
+(* 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 *)
     else
       special@[node;in_modkeep keep]   (* otherwise *)
@@ -779,7 +572,7 @@ let end_module id =
 
     if (fst newoname) <> (fst oldoname) then
       anomaly "Names generated on start_ and end_module do not match";
-    if mp_of_kn (snd newoname) <> mp then 
+    if mp_of_kn (snd newoname) <> mp then
       anomaly "Kernel and Library names do not match";
 
     Lib.add_frozen_state () (* to prevent recaching *);
@@ -787,7 +580,7 @@ let end_module id =
 
 
 
-let module_objects mp = 
+let module_objects mp =
   let prefix,objects = MPmap.find mp !modtab_objects in
     segment_of_objects prefix objects
 
@@ -799,63 +592,67 @@ let module_objects mp =
 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
+type library_objects =
+    module_path * lib_objects * lib_objects
 
 
 let register_library dir cenv objs digest =
   let mp = MPfile dir in
+  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 start_library dir =
   let mp = Global.start_library dir in
-  openmod_info:=[],None,None;
+  openmod_info:=mp,[],None,[];
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
+let end_library_hook = ref ignore
+let set_end_library_hook f = end_library_hook := f
 
-let end_library dir = 
+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 *)
 
 
-let really_import_module mp = 
+let really_import_module mp =
   let prefix,objects = MPmap.find mp !modtab_objects in
     open_objects 1 prefix objects
 
 
-let cache_import (_,(_,mp)) = 
-(* for non-substitutive exports: 
+let cache_import (_,(_,mp)) =
+(* for non-substitutive exports:
   let mp = Nametab.locate_module (qualid_of_dirpath dir) in  *)
   really_import_module mp
 
-let classify_import (_,(export,_ as obj)) = 
+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')
-	
-let (in_import,out_import) = 
+
+let (in_import,_) =
   declare_object {(default_object "IMPORT MODULE") with
 		    cache_function = cache_import;
 		    open_function = (fun i o -> if i=1 then cache_import o);
@@ -863,125 +660,89 @@ let (in_import,out_import) =
 		    classify_function = classify_import }
 
 
-let import_module export mp = 
+let import_module export mp =
   Lib.add_anonymous_leaf (in_import (export,mp))
 
 (************************************************************************)
 (* module types *)
-let start_modtype interp_modtype id args =
-  let fs = Summary.freeze_summaries () in
 
+let start_modtype_ interp_modtype id args mtys fs =
   let mp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
+  let sub_mty_l = build_subtypes interp_modtype mp arg_entries mtys in
   let mbids = List.map fst arg_entries in
-  openmodtype_info := mbids;
+  openmodtype_info := mbids, sub_mty_l;
   let prefix = Lib.start_modtype id mp fs in
   Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix);
   Lib.add_frozen_state (); mp
 
 
-let end_modtype id =
-
-  let oldoname,prefix,fs,lib_stack = Lib.end_modtype id in
-  let ln = Global.end_modtype id in
+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
-
-  Summary.module_unfreeze_summaries fs;
-
-  let modtypeobjs = empty_subst, mbids, msid, substitute in
-
-  let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in
+  let mbids, sub_mty_l = !openmodtype_info in
+  let mp = Global.end_modtype fs id in
+  let modtypeobjs = mbids, mp, substitute in
+  check_subtypes_mt mp sub_mty_l;
+  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 = 
-  let fs = Summary.freeze_summaries () in
 
-  try
+let declare_modtype_ interp_modtype id args mtys (mty,inl) fs =
   let mmp = Global.start_modtype id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
-
-  let base_mty = interp_modtype (Global.env()) mty in
-  let entry = 
-    List.fold_right 
-      (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-      arg_entries
-      base_mty
-  in
-  let substobjs = get_modtype_substobjs (Global.env()) entry in
+  let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in
+  (* NB: check of subtyping will be done in cache_modtype *)
+  let sub_mty_l = build_subtypes interp_modtype mmp arg_entries mtys in
+  let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp inl entry in
   (* Undo the simulated interactive building of the module type *)
   (* and declare the module type as a whole *)
+
+  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)));
+  ignore (add_leaf id (in_modtype (Some (entry,inl), substobjs, sub_mty_l)));
   mmp
-  with e ->
-    (* Something wrong: undo the whole process *)
-    Summary.unfreeze_summaries fs; raise e
-			       
 
-let rec get_module_substobjs env = function
-  | MSEident mp -> MPmap.find mp !modtab_substobjs 
+
+(* 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 mp_from inl = 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 mbid,mbids = 
-	(match mbids with
-	   | mbid::mbids ->mbid,mbids
-	       
-	   | [] -> match mexpr with
-	       | MSEident _  -> error "Application of a non-functor"
-	       | _ -> error "Application of a functor with too few arguments") in
-      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 (Some resolve))
-	else
-	  let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
-	  let sub_alias' =  update_subst sub_alias sub1' in
-		     join sub1' sub_alias'
+       let (mbids, mp, objs) = get_module_substobjs env mp_from inl mexpr in
+	(mbid::mbids, mp, objs)
+  | MSEapply (fexpr, MSEident mp) as me ->
+      let (mbids, mp1, objs),mb_mp1,mp_l =
+	get_objs_module_application env me
       in
-      let sub3 = join sub3 (update_subst sub_alias 
-			      (map_mbid farg_id mp (Some resolve))) 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)
-  | 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
-
+      let mbids_left,subst =
+	compute_subst env mbids mb_mp1.mod_type (List.rev mp_l) inl in
+      (mbids_left, mp1,subst_objects subst objs)
+  | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr
+  | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from inl mty
+  | MSEwith (mty, With_Module (idl,mp)) -> assert false
 
 (* Include *)
 
@@ -995,58 +756,43 @@ let rec subst_inc_expr subst me =
 	let const1 = Mod_subst.from_val const in
 	let force = Mod_subst.force subst_mps in
 	MSEwith (subst_inc_expr subst me,
-		 With_Definition(idl,force (subst_substituted 
+		 With_Definition(idl,force (subst_substituted
 					   subst const1)))
-    | MSEapply (me1,me2) -> 
+    | MSEapply (me1,me2) ->
 	MSEapply (subst_inc_expr subst me1,
 		  subst_inc_expr subst me2)
-    | _ -> anomaly "You cannot Include a high-order structure"
+    | MSEfunctor(mbid,me1,me2) ->
+        MSEfunctor (mbid, subst_inc_expr subst me1, subst_inc_expr subst me2)
 
 let lift_oname (sp,kn) =
   let mp,_,_ = Names.repr_kn kn in
   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)
+    open_objects i prefix objs
+      
+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
@@ -1054,137 +800,182 @@ let (in_include,out_include) =
     load_function = load_include;
     open_function = open_include;
     subst_function = subst_include;
-    classify_function = classify_include;
-    export_function = (fun _ -> anomaly "No modules in section!") }
-
-let rec update_include (sub,mbids,msid,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 substobjs' = update_include substobjs in
-            (id, in_include ((me,true),substobjs',substituted))::
-	      (replace_include tail)
-	else
-	  (id,obj)::(replace_include tail)
-  in
-    (sub,mbids,msid,replace_include objs)
-      
-      
-      
-let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
-  
-  let fs = Summary.freeze_summaries () in
+    classify_function = classify_include }
 
-  try
+
+let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs =
   let mmp = Global.start_module id in
   let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
 
-  let mty_entry_o, mty_sub_o = match mty_o with
-      None -> None, None
-    | (Some (mty, true)) -> 
-	Some (List.fold_right 
-		(fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-		arg_entries 
-		(interp_modtype (Global.env()) mty)), 
-	None
-    | (Some (mty, false)) -> 
-	None, 
-	Some (List.fold_right 
-		(fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte))
-		arg_entries 
-		(interp_modtype (Global.env()) mty))
+  let funct f m = funct_entry arg_entries (f (Global.env ()) m) in
+  let env = Global.env() in
+  let mty_entry_o, subs, inl_res = match res with
+    | Topconstr.Enforce (mty,inl) -> Some (funct interp_modtype mty), [], inl
+    | Topconstr.Check mtys ->
+	None, build_subtypes interp_modtype mmp arg_entries mtys, true
   in
-  let mexpr_entry_o = match mexpr_o with
-      None -> None
-    | Some mexpr -> 
-	Some (List.fold_right 
-		(fun (mbid,mte) me -> MSEfunctor(mbid,mte,me))
-		arg_entries
-		(interp_modexpr (Global.env()) mexpr))
+ 
+  (*let subs = List.map (Mod_typing.translate_module_type env mmp) mty_sub_l in  *)
+  let mexpr_entry_o, inl_expr = match mexpr_o with
+    | None -> None, true
+    | Some (mexpr, inl) -> Some (funct interp_modexpr mexpr), inl
   in
-  let entry = 
-    {mod_entry_type = mty_entry_o;	    
+  let entry =
+    {mod_entry_type = mty_entry_o;
      mod_entry_expr = mexpr_entry_o }
   in
-  let env = Global.env() in
-  let substobjs =
+
+  let(mbids,mp_from,objs) =
     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 inl_res mte
+      | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mmp inl_expr mexpr
       | _ -> anomaly "declare_module: No type, no body ..."
   in
-  let substobjs = 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 = (join sub 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 -> 
+  (* Undo the simulated interactive building of the module *)
+  (* and declare the module as a whole *)
+  Summary.unfreeze_summaries fs;
+  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 (inl_expr&&inl_res) in
+
+  if mp_env <> mp then anomaly "Kernel and Library names do not match";
+
+  
+  check_subtypes mp subs;
+
+  let substobjs = (mbids,mp_env,
+		   subst_objects(map_mp mp_from mp_env resolver) objs) in
+  ignore (add_leaf
+	    id
+	    (in_module (Some (entry), substobjs)));
+  mmp
+
+
+let rec include_subst env mb mbids sign inline =
+  match mbids with
+    | [] -> empty_subst
+    | mbid::mbids ->
+	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+	let subst = include_subst env mb mbids fbody_b inline in
+	let mp_delta = if not inline then mb.mod_delta else
+	  Modops.complete_inline_delta_resolver env mb.mod_mp
+	    farg_id farg_b mb.mod_delta
+	in
+	join (map_mbid mbid mb.mod_mp mp_delta) subst
+
+exception NothingToDo
+
+let get_includeself_substobjs env objs me is_mod inline =
+  try
+    let mb_mp = match me with
+      | MSEident mp ->
+	  if is_mod then
+	    Environ.lookup_module mp env
+	  else
+	    Modops.module_body_of_type mp (Environ.lookup_modtype mp env)
+      | MSEapply(fexpr, MSEident p) as mexpr ->
+	  let _,mb_mp,mp_l =
+	    if is_mod then
+	      get_objs_module_application env mexpr
+	    else
+	      let o,mtb_mp,mp_l = get_objs_modtype_application env mexpr in
+	      o,Modops.module_body_of_type mtb_mp.typ_mp mtb_mp,mp_l
+	  in
+	  List.fold_left
+	    (fun mb _ ->
+	       match mb.mod_type with
+		 |  SEBfunctor(_,_,str) -> {mb with mod_type = str}
+		 | _ -> error "Application of a functor with too much arguments.")
+	    mb_mp mp_l
+      | _ -> raise NothingToDo
+    in
+    let (mbids,mp_self,objects) = objs in
+    let mb = Global.pack_module() in
+    let subst = include_subst env mb mbids mb_mp.mod_type inline in
+    ([],mp_self,subst_objects subst objects)
+  with NothingToDo -> objs
+
+let declare_one_include_inner inl (me,is_mod) =
+  let env = Global.env() in
+  let mp1,_ = current_prefix () in
+  let (mbids,mp,objs)=
+    if is_mod then
+      get_module_substobjs env mp1 inl me
+    else
+      get_modtype_substobjs env mp1 inl me in
+  let (mbids,mp,objs) =
+    if mbids <> [] then
+      get_includeself_substobjs env (mbids,mp,objs) me is_mod inl
+    else
+      (mbids,mp,objs) in
+  let id = current_mod_id() in
+  let resolver =  Global.add_include me is_mod inl in
+  let substobjs = (mbids,mp1,
+		   subst_objects (map_mp mp mp1 resolver) objs) in
+  ignore (add_leaf id
+	    (in_include ((me,is_mod), substobjs)))
+
+let declare_one_include interp_struct me_ast =
+  declare_one_include_inner (snd me_ast)
+    (interp_struct (Global.env()) (fst me_ast))
+
+let declare_include_ interp_struct me_asts =
+  List.iter (declare_one_include interp_struct) me_asts
+
+(** Versions of earlier functions taking care of the freeze/unfreeze
+    of summaries *)
+
+let protect_summaries f =
+  let fs = Summary.freeze_summaries () in
+  try f fs
+  with e ->
     (* Something wrong: undo the whole process *)
     Summary.unfreeze_summaries fs; raise e
-      
 
-let declare_include interp_struct me_ast is_mod =
+let declare_include interp_struct me_asts =
+  protect_summaries
+    (fun _ -> declare_include_ interp_struct me_asts)
+
+let declare_modtype interp_mt interp_mix id args mtys mty_l =
+  let declare_mt fs = match mty_l with
+    | [] -> assert false
+    | [mty] -> declare_modtype_ interp_mt id args mtys mty fs
+    | mty_l ->
+	ignore (start_modtype_ interp_mt id args mtys fs);
+	declare_include_ interp_mix mty_l;
+	end_modtype ()
+  in
+  protect_summaries declare_mt
+
+let start_modtype interp_modtype id args mtys =
+  protect_summaries (start_modtype_ interp_modtype id args mtys)
+
+let declare_module interp_mt interp_me interp_mix id args mtys me_l =
+  let declare_me fs = match me_l with
+    | [] -> declare_module_ interp_mt interp_me id args mtys None fs
+    | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs
+    | me_l ->
+	ignore (start_module_ interp_mt None id args mtys fs);
+	declare_include_ interp_mix me_l;
+	end_module ()
+  in
+  protect_summaries declare_me
+
+let start_module interp_modtype export id args res =
+ protect_summaries (start_module_ interp_modtype export id args res)
 
-  let fs = Summary.freeze_summaries () in
 
-    try 
-      let env = Global.env() in
-      let me = interp_struct env me_ast in 
-      let substobjs = 	
-	if is_mod then
-	  get_module_substobjs env 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
-      let id = current_mod_id() in
-	
-	ignore (add_leaf id
-		  (in_include ((me,is_mod), substobjs, substituted)))
-    with e -> 
-      (* Something wrong: undo the whole process *)
-      Summary.unfreeze_summaries fs; raise e
-	
-	
 (*s Iterators. *)
-	
+
 let iter_all_segments f =
-  let _ = 
-    MPmap.iter 
-      (fun _ (prefix,objects) -> 
-	 let apply_obj (id,obj) = f (make_oname prefix id) obj in
+  let _ =
+    MPmap.iter
+      (fun _ (prefix,objects) ->
+	 let rec apply_obj (id,obj) = match object_tag obj with 
+	   | "INCLUDE" -> 
+	       let (_,(_,_,objs)) =  out_include obj in 
+		 List.iter apply_obj objs
+		   
+	   | _ -> f (make_oname prefix id) obj in
 	   List.iter apply_obj objects)
       !modtab_objects
   in