This big commit addresses two problems:

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

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

Module M := P.

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

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

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

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


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


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



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

1 files changed, 238 insertions, 264 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e73689bc8c..b0dc6dd8a0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -35,13 +35,12 @@ type modvariant =
   | LIBRARY of dir_path
 
 type module_info =
-    { msid : mod_self_id;
-      modpath : module_path;
-      seed : dir_path; (* the "seed" of unique identifier generator *)
-      label : label;
-      variant : modvariant;
-      alias_subst : substitution}
-
+    {modpath : module_path;
+     label : label;
+     variant : modvariant;
+     resolver : delta_resolver;
+     resolver_of_param : delta_resolver;}
+      
 let check_label l labset =
   if Labset.mem l labset then error_existing_label l
 
@@ -80,12 +79,11 @@ let rec empty_environment =
   { old = empty_environment;
     env = empty_env;
     modinfo = {
-      msid = initial_msid;
       modpath = initial_path;
-      seed = initial_dir;
       label = mk_label "_";
       variant = NONE;
-      alias_subst = empty_subst};
+      resolver = empty_delta_resolver;
+      resolver_of_param = empty_delta_resolver};
     labset = Labset.empty;
     revstruct = [];
     univ = Univ.Constraint.empty;
@@ -215,9 +213,16 @@ let add_constant dir l decl senv =
   in
   let senv' = add_constraints cb.const_constraints senv in
   let env'' = Environ.add_constant kn cb senv'.env in
+  let resolver = 
+    if cb.const_inline then
+      add_inline_delta_resolver kn senv'.modinfo.resolver
+    else
+      senv'.modinfo.resolver
+  in
     kn, { old = senv'.old;
 	  env = env'';
-	  modinfo = senv'.modinfo;
+	  modinfo = {senv'.modinfo with
+		       resolver = resolver};
 	  labset = Labset.add l senv'.labset;
 	  revstruct = (l,SFBconst cb)::senv'.revstruct;
           univ = senv'.univ;
@@ -242,7 +247,7 @@ let add_mind dir l mie senv =
        all labels *)
   let mib = translate_mind senv.env mie in
   let senv' = add_constraints mib.mind_constraints senv in
-  let kn = make_kn senv.modinfo.modpath dir l in
+  let kn = make_mind senv.modinfo.modpath dir l in
   let env'' = Environ.add_mind kn mib senv'.env in
   kn, { old = senv'.old;
 	env = env'';
@@ -259,118 +264,82 @@ let add_mind dir l mie senv =
 
 let add_modtype l mte senv =
   check_label l senv.labset;
-  let mtb_expr,sub = translate_struct_entry senv.env mte  in
-  let mtb = { typ_expr = mtb_expr;
-	      typ_strength = None;
-	      typ_alias = sub} in
-  let senv' = add_constraints
-    (struct_expr_constraints mtb_expr) senv in
   let mp = MPdot(senv.modinfo.modpath, l) in
-  let env'' = Environ.add_modtype mp mtb senv'.env in
-  mp, { old = senv'.old;
-	env = env'';
-	modinfo = senv'.modinfo;
-	labset = Labset.add l senv'.labset;
-	revstruct = (l,SFBmodtype mtb)::senv'.revstruct;
-        univ = senv'.univ;
-        engagement = senv'.engagement;
-	imports = senv'.imports;
-	loads = senv'.loads;
-        local_retroknowledge = senv'.local_retroknowledge }
+  let mtb = translate_module_type senv.env mp mte  in
+  let senv' = add_constraints mtb.typ_constraints senv in
+   let env'' = Environ.add_modtype mp mtb senv'.env in
+    mp, { old = senv'.old;
+	  env = env'';
+	  modinfo = senv'.modinfo;
+	  labset = Labset.add l senv'.labset;
+	  revstruct = (l,SFBmodtype mtb)::senv'.revstruct;
+          univ = senv'.univ;
+          engagement = senv'.engagement;
+	  imports = senv'.imports;
+	  loads = senv'.loads;
+          local_retroknowledge = senv'.local_retroknowledge }
 
 
 (* full_add_module adds module with universes and constraints *)
-let full_add_module mp mb senv =
-  let senv = add_constraints (module_constraints mb) senv in
-  let env = Modops.add_module mp mb senv.env in
+let full_add_module mb senv =
+  let senv = add_constraints mb.mod_constraints senv in
+  let env = Modops.add_module mb senv.env in
     {senv with env = env}
 
 (* Insertion of modules *)
 
 let add_module l me senv =
   check_label l senv.labset;
-  let mb = translate_module senv.env me in
   let mp = MPdot(senv.modinfo.modpath, l) in
-  let senv' = full_add_module mp mb senv in
-  let is_functor,sub = Modops.update_subst senv'.env mb mp in
-  mp, { old = senv'.old;
-	env = senv'.env;
-	modinfo =
-      if is_functor then
-	senv'.modinfo
-      else
-	{senv'.modinfo with
-	   alias_subst = join senv'.modinfo.alias_subst sub};
-	labset = Labset.add l senv'.labset;
-	revstruct = (l,SFBmodule mb)::senv'.revstruct;
-        univ = senv'.univ;
-        engagement = senv'.engagement;
-	imports = senv'.imports;
-	loads = senv'.loads;
-        local_retroknowledge = senv'.local_retroknowledge }
-
-let add_alias l mp senv =
-  check_label l senv.labset;
-  let mp' = MPdot(senv.modinfo.modpath, l) in
-  let mp1 = scrape_alias mp senv.env in
-  let typ_opt =
-    if check_bound_mp mp then
-      Some (strengthen senv.env
-	      (lookup_modtype mp senv.env).typ_expr mp)
-    else
-      None
+  let mb = translate_module senv.env mp me in
+  let senv' = full_add_module mb senv  in
+  let modinfo = match mb.mod_type with
+      SEBstruct _ -> 
+	{ senv'.modinfo with
+	    resolver = 
+	    add_delta_resolver mb.mod_delta senv'.modinfo.resolver}
+    | _ -> senv'.modinfo
   in
-    (* we get all updated alias substitution {mp1.K\M}  that comes from mp1 *)
-  let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in
-    (* transformation of {mp1.K\M} to {mp.K\M}*)
-  let sub = update_subst sub (map_mp mp' mp1) in
-   (* transformation of {mp.K\M}  to {mp.K\M'} where M'=M{mp1\mp'}*)
-  let sub = join_alias sub (map_mp mp' mp1) in
-    (* we add the alias substitution  *)
-  let sub = add_mp mp' mp1 sub in
-  let env' = register_alias mp' mp senv.env in
-    mp', { old = senv.old;
-	env = env';
-	modinfo = { senv.modinfo with
-		      alias_subst = join
-	    senv.modinfo.alias_subst sub};
-	labset = Labset.add l senv.labset;
-	revstruct = (l,SFBalias (mp,typ_opt,None))::senv.revstruct;
-        univ = senv.univ;
-        engagement = senv.engagement;
-	imports = senv.imports;
-	loads = senv.loads;
-        local_retroknowledge = senv.local_retroknowledge }
-
+    mp,mb.mod_delta,
+  { old = senv'.old;
+    env = senv'.env;
+    modinfo = modinfo;
+    labset = Labset.add l senv'.labset;
+    revstruct = (l,SFBmodule mb)::senv'.revstruct;
+    univ = senv'.univ;
+    engagement = senv'.engagement;
+    imports = senv'.imports;
+    loads = senv'.loads;
+    local_retroknowledge = senv'.local_retroknowledge }
+    
 (* Interactive modules *)
 
 let start_module l senv =
   check_label l senv.labset;
-  let msid = make_msid senv.modinfo.seed (string_of_label l) in
-  let mp = MPself msid in
-  let modinfo = { msid = msid;
-		  modpath = mp;
-		  seed = senv.modinfo.seed;
-		  label = l;
-		  variant = STRUCT [];
-		  alias_subst = empty_subst}
-  in
-  mp, { old = senv;
-	env = senv.env;
-	modinfo = modinfo;
-	labset = Labset.empty;
-	revstruct = [];
-        univ = Univ.Constraint.empty;
-        engagement = None;
-	imports = senv.imports;
-	loads = [];
-	(* spiwack : not sure, but I hope it's correct *)
-        local_retroknowledge = [] }
+ let mp = MPdot(senv.modinfo.modpath, l) in
+ let modinfo = { modpath = mp;
+		 label = l;
+		 variant = STRUCT [];
+		 resolver = empty_delta_resolver;
+		 resolver_of_param = empty_delta_resolver}
+ in
+   mp, { old = senv;
+	 env = senv.env;
+	 modinfo = modinfo;
+	 labset = Labset.empty;
+	 revstruct = [];
+         univ = Univ.Constraint.empty;
+         engagement = None;
+	 imports = senv.imports;
+	 loads = [];
+	 (* spiwack : not sure, but I hope it's correct *)
+         local_retroknowledge = [] }
 
 let end_module l restype senv =
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
-  let restype = Option.map (translate_struct_entry senv.env) restype in
+  let mp = senv.modinfo.modpath in
+  let restype = Option.map (translate_module_type senv.env mp) restype in
   let params,is_functor =
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
@@ -386,83 +355,107 @@ let end_module l restype senv =
       params
   in
    let auto_tb =
-     SEBstruct (modinfo.msid, List.rev senv.revstruct)
+     SEBstruct (List.rev senv.revstruct)
   in
-  let mod_typ,subst,cst =
+   let mexpr,mod_typ,mod_typ_alg,resolver,cst = 
     match restype with
-      | None ->  None,modinfo.alias_subst,Constraint.empty
-      | Some (res_tb,subst) ->
-	  let cst = check_subtypes senv.env
-	    {typ_expr = auto_tb;
-	     typ_strength = None;
-	     typ_alias = modinfo.alias_subst}
-	    {typ_expr = res_tb;
-	     typ_strength = None;
-	     typ_alias = subst} in
-	  let mtb = functorize_struct res_tb in
-	    Some mtb,subst,cst
+      | None ->  let mexpr = functorize_struct auto_tb in
+	 mexpr,mexpr,None,modinfo.resolver,Constraint.empty
+      | Some mtb ->
+	  let auto_mtb = {
+	    typ_mp = senv.modinfo.modpath;
+	    typ_expr = auto_tb;
+	    typ_expr_alg = None;
+	    typ_constraints = Constraint.empty;
+	    typ_delta = empty_delta_resolver} in
+	  let cst = check_subtypes senv.env auto_mtb
+	    mtb in
+	  let mod_typ = functorize_struct mtb.typ_expr in
+	  let mexpr = functorize_struct auto_tb in
+	  let typ_alg = 
+	    Option.map functorize_struct mtb.typ_expr_alg in
+	    mexpr,mod_typ,typ_alg,mtb.typ_delta,cst
   in
-  let mexpr = functorize_struct auto_tb in
   let cst = Constraint.union cst senv.univ in
   let mb =
-    { mod_expr = Some mexpr;
+    { mod_mp = mp;
+      mod_expr = Some mexpr;
       mod_type = mod_typ;
+      mod_type_alg = mod_typ_alg;
       mod_constraints = cst;
-      mod_alias = subst;
+      mod_delta = resolver;
       mod_retroknowledge = senv.local_retroknowledge }
   in
-  let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
   let newenv = set_engagement_opt senv.engagement newenv in
   let senv'= {senv with env=newenv} in
   let senv' =
     List.fold_left
-      (fun env (mp,mb) -> full_add_module mp mb env)
+      (fun env (_,mb) -> full_add_module mb env) 
       senv'
       (List.rev senv'.loads)
   in
   let newenv = Environ.add_constraints cst senv'.env in
   let newenv =
-    Modops.add_module mp mb newenv
-  in
-  let is_functor,subst = Modops.update_subst newenv mb mp in
-  let newmodinfo =
-    if is_functor then
-      oldsenv.modinfo
-    else
-      { oldsenv.modinfo with
-	  alias_subst = join
-	  oldsenv.modinfo.alias_subst
-	  subst };
+    Modops.add_module mb newenv in 
+  let modinfo = match mb.mod_type with
+      SEBstruct _ -> 
+	{ oldsenv.modinfo with
+	    resolver = 
+	    add_delta_resolver resolver oldsenv.modinfo.resolver}
+    | _ -> oldsenv.modinfo
   in
-    mp, { old = oldsenv.old;
-	env = newenv;
-	modinfo = newmodinfo;
-	labset = Labset.add l oldsenv.labset;
-	revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
-        univ = Univ.Constraint.union senv'.univ oldsenv.univ;
-        (* engagement is propagated to the upper level *)
-        engagement = senv'.engagement;
-	imports = senv'.imports;
-	loads = senv'.loads@oldsenv.loads;
-	local_retroknowledge = senv'.local_retroknowledge@oldsenv.local_retroknowledge }
+    mp,resolver,{ old = oldsenv.old;
+		  env = newenv;
+		  modinfo = modinfo;
+		  labset = Labset.add l oldsenv.labset;
+		  revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
+		  univ = Univ.Constraint.union senv'.univ oldsenv.univ;
+		  (* engagement is propagated to the upper level *)
+		  engagement = senv'.engagement;
+		  imports = senv'.imports;
+		  loads = senv'.loads@oldsenv.loads;
+		  local_retroknowledge = 
+	senv'.local_retroknowledge@oldsenv.local_retroknowledge }
 
 
 (* Include for module and module type*)
- let add_include me senv =
-   let struct_expr,_ =  translate_struct_entry senv.env me in
-   let senv = add_constraints (struct_expr_constraints struct_expr) senv in
-   let msid,str = match (eval_struct senv.env struct_expr) with
-     | SEBstruct(msid,str_l) -> msid,str_l
-     | _ -> error ("You cannot Include a higher-order Module or Module Type.")
+ let add_include me is_module senv =
+   let sign,cst,resolver =
+     if is_module then
+       let sign,resolver,cst =  
+	 translate_struct_include_module_entry senv.env 
+	   senv.modinfo.modpath me in
+	 sign,cst,resolver
+     else
+       let mtb = 
+	 translate_module_type senv.env 
+	   senv.modinfo.modpath me in
+	 mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
    in
+   let senv = add_constraints cst senv in
    let mp_sup = senv.modinfo.modpath in
-   let str1 = subst_signature_msid msid mp_sup str in
+   let str = match sign with
+     | SEBstruct(str_l) ->
+	 str_l
+     | _ -> error ("You cannot Include a high-order structure.")
+   in
+   let senv =
+     {senv 
+      with modinfo = 
+	 {senv.modinfo
+	  with resolver =
+	     add_delta_resolver resolver senv.modinfo.resolver}}
+   in
    let add senv (l,elem)  =
      check_label l senv.labset;
      match elem with
        | SFBconst cb ->
-	   let con = make_con mp_sup empty_dirpath l in
+	   let kn = make_kn mp_sup empty_dirpath l in
+	   let con = constant_of_kn_equiv kn
+	     (canonical_con 
+		(constant_of_delta resolver (constant_of_kn kn)))
+	   in
 	   let senv' = add_constraints cb.const_constraints senv in
 	   let env'' = Environ.add_constant con cb senv'.env in
 	     { old = senv'.old;
@@ -475,11 +468,14 @@ let end_module l restype senv =
 	       imports = senv'.imports;
 	       loads = senv'.loads ;
 	       local_retroknowledge = senv'.local_retroknowledge }
-
        | SFBmind mib ->
 	   let kn = make_kn mp_sup empty_dirpath l in
+	   let mind = mind_of_kn_equiv kn
+	     (canonical_mind 
+		(mind_of_delta resolver (mind_of_kn kn)))
+	   in
 	   let senv' = add_constraints mib.mind_constraints senv in
-	   let env'' = Environ.add_mind kn mib senv'.env in
+	   let env'' = Environ.add_mind mind mib senv'.env in
 	     { old = senv'.old;
 	       env = env'';
 	       modinfo = senv'.modinfo;
@@ -492,17 +488,10 @@ let end_module l restype senv =
                local_retroknowledge = senv'.local_retroknowledge }
 
        | SFBmodule mb ->
-	   let mp = MPdot(senv.modinfo.modpath, l) in
-	   let is_functor,sub = Modops.update_subst senv.env mb mp in
-	   let senv' = full_add_module mp mb senv in
+	   let senv' = full_add_module mb senv in
 	     { old = senv'.old;
 	       env = senv'.env;
-	       modinfo =
-		 if is_functor then
-		   senv'.modinfo
-		 else
-		   {senv'.modinfo with
-		      alias_subst = join senv'.modinfo.alias_subst sub};
+	       modinfo = senv'.modinfo;
 	       labset = Labset.add l senv'.labset;
 	       revstruct = (l,SFBmodule mb)::senv'.revstruct;
 	       univ = senv'.univ;
@@ -510,87 +499,69 @@ let end_module l restype senv =
 	       imports = senv'.imports;
 	       loads = senv'.loads;
 	       local_retroknowledge = senv'.local_retroknowledge }
-       | SFBalias (mp',typ_opt,cst) ->
-	   let env' = Option.fold_right
-	     Environ.add_constraints cst senv.env in
-	   let mp = MPdot(senv.modinfo.modpath, l) in
-	   let mp1 = scrape_alias mp' senv.env in
-	   let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in
-	   let sub = update_subst sub (map_mp mp mp1) in
-	   let sub = join_alias sub (map_mp mp mp1) in
-	   let sub = add_mp mp mp1 sub in
-	   let env' = register_alias mp mp' env' in
-	     { old = senv.old;
-	       env = env';
-	       modinfo =  { senv.modinfo with
-			      alias_subst = join
-		   senv.modinfo.alias_subst sub};
-	       labset = Labset.add l senv.labset;
-	       revstruct = (l,SFBalias (mp',typ_opt,cst))::senv.revstruct;
-               univ = senv.univ;
-               engagement = senv.engagement;
-	       imports = senv.imports;
-	       loads = senv.loads;
-               local_retroknowledge = senv.local_retroknowledge }
        | SFBmodtype mtb ->
-	   let env' = add_modtype_constraints senv.env mtb in
+	   let senv' = add_constraints mtb.typ_constraints senv in
 	   let mp = MPdot(senv.modinfo.modpath, l) in
-	   let env'' = Environ.add_modtype mp mtb env' in
+	   let env' = Environ.add_modtype mp mtb senv'.env in
 	     { old = senv.old;
-	       env = env'';
-	       modinfo = senv.modinfo;
+	       env = env';
+	       modinfo = senv'.modinfo;
 	       labset = Labset.add l senv.labset;
-	       revstruct = (l,SFBmodtype mtb)::senv.revstruct;
-               univ = senv.univ;
-               engagement = senv.engagement;
-	       imports = senv.imports;
-	       loads = senv.loads;
-               local_retroknowledge = senv.local_retroknowledge }
+	       revstruct = (l,SFBmodtype mtb)::senv'.revstruct;
+               univ = senv'.univ;
+               engagement = senv'.engagement;
+	       imports = senv'.imports;
+	       loads = senv'.loads;
+               local_retroknowledge = senv'.local_retroknowledge }
    in
-     List.fold_left add senv str1
+     resolver,(List.fold_left add senv str)
 
 (* Adding parameters to modules or module types *)
 
 let add_module_parameter mbid mte senv =
   if  senv.revstruct <> [] or senv.loads <> [] then
     anomaly "Cannot add a module parameter to a non empty module";
-  let mtb_expr,sub = translate_struct_entry senv.env mte in
-  let mtb = {typ_expr = mtb_expr;
-	    typ_strength = None;
-	    typ_alias = sub} in
-  let senv = full_add_module (MPbound mbid) (module_body_of_type mtb) senv
+  let mtb = translate_module_type senv.env (MPbound mbid) mte in
+  let senv = 
+    full_add_module (module_body_of_type (MPbound mbid) mtb) senv
   in
   let new_variant = match senv.modinfo.variant with
     | STRUCT params -> STRUCT ((mbid,mtb) :: params)
     | SIG params -> SIG ((mbid,mtb) :: params)
     | _ ->
-	anomaly "Module parameters can only be added to modules or signatures"
+	anomaly "Module parameters can only be added to modules or signatures"  
   in
-  { old = senv.old;
-    env = senv.env;
-    modinfo = { senv.modinfo with variant = new_variant };
-    labset = senv.labset;
-    revstruct = [];
-    univ = senv.univ;
-    engagement = senv.engagement;
-    imports = senv.imports;
-    loads = [];
-    local_retroknowledge = senv.local_retroknowledge }
-
+    
+  let resolver_of_param = match mtb.typ_expr with
+      SEBstruct _ -> mtb.typ_delta
+    | _ -> empty_delta_resolver
+  in
+    mtb.typ_delta, { old = senv.old;
+		     env = senv.env;
+		     modinfo = { senv.modinfo with 
+				   variant = new_variant;
+				   resolver_of_param = add_delta_resolver
+			      resolver_of_param senv.modinfo.resolver_of_param};
+		     labset = senv.labset;
+		     revstruct = [];
+		     univ = senv.univ;
+		     engagement = senv.engagement;
+		     imports = senv.imports;
+		     loads = [];
+		     local_retroknowledge = senv.local_retroknowledge }
+      
 
 (* Interactive module types *)
 
 let start_modtype l senv =
   check_label l senv.labset;
-  let msid = make_msid senv.modinfo.seed (string_of_label l) in
-  let mp = MPself msid in
-  let modinfo = { msid = msid;
-		  modpath = mp;
-		  seed = senv.modinfo.seed;
-		  label = l;
-		  variant = SIG [];
-		  alias_subst = empty_subst }
-  in
+ let mp = MPdot(senv.modinfo.modpath, l) in
+ let modinfo = { modpath = mp;
+		 label = l;
+		 variant = SIG [];
+		 resolver = empty_delta_resolver;
+		 resolver_of_param = empty_delta_resolver}
+ in
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
@@ -614,7 +585,7 @@ let end_modtype l senv =
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_local_context None;
   let auto_tb =
-     SEBstruct (modinfo.msid, List.rev senv.revstruct)
+     SEBstruct (List.rev senv.revstruct)
   in
   let mtb_expr =
     List.fold_left
@@ -625,42 +596,39 @@ let end_modtype l senv =
   in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
-  (* since universes constraints cannot be stored in the modtype,
-     they are propagated to the upper level *)
   let newenv = Environ.add_constraints senv.univ  newenv in
   let newenv = set_engagement_opt senv.engagement newenv in
   let senv = {senv with env=newenv} in
   let senv =
     List.fold_left
-      (fun env (mp,mb) -> full_add_module mp mb env)
+      (fun env (mp,mb) -> full_add_module mb env)
       senv
       (List.rev senv.loads)
   in
-  let subst = senv.modinfo.alias_subst in
-  let mtb = {typ_expr = mtb_expr;
-	    typ_strength = None;
-	    typ_alias = subst} in
+  let mtb = {typ_mp = mp;
+    typ_expr = mtb_expr;
+    typ_expr_alg = None;
+    typ_constraints = senv.univ;
+    typ_delta = senv.modinfo.resolver} in
   let newenv =
     Environ.add_modtype mp mtb senv.env
   in
     mp, { old = oldsenv.old;
 	  env = newenv;
-	modinfo = oldsenv.modinfo;
-	labset = Labset.add l oldsenv.labset;
-	revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
-        univ = Univ.Constraint.union senv.univ oldsenv.univ;
-        engagement = senv.engagement;
-	imports = senv.imports;
-	loads = senv.loads@oldsenv.loads;
-        (* spiwack : if there is a bug with retroknowledge in nested modules
-                     it's likely to come from here *)
-        local_retroknowledge =
-                   senv.local_retroknowledge@oldsenv.local_retroknowledge}
-
+	  modinfo = oldsenv.modinfo;
+	  labset = Labset.add l oldsenv.labset;
+	  revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
+          univ = Univ.Constraint.union senv.univ oldsenv.univ;
+          engagement = senv.engagement;
+	  imports = senv.imports;
+	  loads = senv.loads@oldsenv.loads;
+          (* spiwack : if there is a bug with retroknowledge in nested modules
+             it's likely to come from here *)
+          local_retroknowledge = 
+        senv.local_retroknowledge@oldsenv.local_retroknowledge}
 
 let current_modpath senv = senv.modinfo.modpath
-let current_msid senv = senv.modinfo.msid
-
+let delta_of_senv senv = senv.modinfo.resolver,senv.modinfo.resolver_of_param
 
 (* Check that the engagement expected by a library matches the initial one *)
 let check_engagement env c =
@@ -685,7 +653,7 @@ type compiled_library =
 
 let is_empty senv =
   senv.revstruct = [] &&
-  senv.modinfo.msid = initial_msid &&
+  senv.modinfo.modpath = initial_path &&
   senv.modinfo.variant = NONE
 
 let start_library dir senv =
@@ -697,14 +665,12 @@ let start_library dir senv =
       | hd::tl ->
 	  make_dirpath tl, label_of_id hd
   in
-  let msid = make_msid dir_path (string_of_label l) in
-  let mp = MPself msid in
-  let modinfo = { msid = msid;
-		  modpath = mp;
-		  seed = dir;
-		  label = l;
-		  variant = LIBRARY dir;
-		  alias_subst = empty_subst }
+  let mp = MPfile dir in
+  let modinfo = {modpath = mp;
+		 label = l;
+		 variant = LIBRARY dir;
+		 resolver = empty_delta_resolver;
+		 resolver_of_param = empty_delta_resolver}
   in
   mp, { old = senv;
 	env = senv.env;
@@ -731,14 +697,18 @@ let export senv dir =
   end;
   (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then
     (* error_export_simple *) (); *)
-  let mb =
-    { mod_expr = Some (SEBstruct (modinfo.msid, List.rev senv.revstruct));
-      mod_type = None;
+    let str = SEBstruct (List.rev senv.revstruct) in
+    let mp = senv.modinfo.modpath in
+    let mb = 
+    { mod_mp = mp;
+      mod_expr = Some str;
+      mod_type = str;
+      mod_type_alg = None;
       mod_constraints = senv.univ;
-      mod_alias = senv.modinfo.alias_subst;
+      mod_delta = senv.modinfo.resolver;
       mod_retroknowledge = senv.local_retroknowledge}
   in
-    modinfo.msid, (dir,mb,senv.imports,engagement senv.env)
+   mp, (dir,mb,senv.imports,engagement senv.env)
 
 
 let check_imports senv needed =
@@ -775,9 +745,13 @@ let import (dp,mb,depends,engmt) digest senv =
   let mp = MPfile dp in
   let env = senv.env in
   let env = Environ.add_constraints mb.mod_constraints env in
-  let env = Modops.add_module mp mb env in
+  let env = Modops.add_module mb env in
   mp, { senv with
 	  env = env;
+	  modinfo = 
+      {senv.modinfo with 
+	 resolver = 
+	    add_delta_resolver mb.mod_delta senv.modinfo.resolver};
 	  imports = (dp,digest)::senv.imports;
 	  loads = (mp,mb)::senv.loads }
 
@@ -785,14 +759,14 @@ let import (dp,mb,depends,engmt) digest senv =
 (* Remove the body of opaque constants in modules *)
  let rec lighten_module mb =
   { mb with
-    mod_expr = Option.map lighten_modexpr mb.mod_expr;
-    mod_type = Option.map lighten_modexpr mb.mod_type;
+    mod_expr = None;
+    mod_type = lighten_modexpr mb.mod_type;
   }
 
 and lighten_struct struc =
   let lighten_body (l,body) = (l,match body with
     | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
-    | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x
+    | (SFBconst _ | SFBmind _ ) as x -> x
     | SFBmodule m -> SFBmodule (lighten_module m)
     | SFBmodtype m -> SFBmodtype
 	({m with
@@ -807,8 +781,8 @@ and lighten_modexpr = function
 			typ_expr = lighten_modexpr mty.typ_expr}),
 		  lighten_modexpr mexpr)
   | SEBident mp as x -> x
-  | SEBstruct (msid, struc) ->
-      SEBstruct (msid, lighten_struct struc)
+  | SEBstruct (struc) ->
+      SEBstruct  (lighten_struct struc)
   | SEBapply (mexpr,marg,u) ->
       SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
   | SEBwith (seb,wdcl) ->