Ajout des alias de module dans le noyau.

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

18 files changed, 680 insertions, 310 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 63c690d485..475ef042d1 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -251,13 +251,14 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBmodtype of struct_expr_body
+  | SFBalias of module_path * constraints option
+  | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
 
 and struct_expr_body =
   | SEBident of module_path
-  | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body 
+  | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body 
   | SEBstruct of mod_self_id * structure_body
   | SEBapply of struct_expr_body * struct_expr_body
       * constraints
@@ -270,8 +271,11 @@ and with_declaration_body =
 and module_body = 
     { mod_expr : struct_expr_body option;
       mod_type : struct_expr_body option;
-      mod_equiv : module_path option;
       mod_constraints : constraints;
+      mod_alias : substitution;
       mod_retroknowledge : Retroknowledge.action list}
 
-type module_type_body = struct_expr_body * module_path option
+and module_type_body = 
+    { typ_expr : struct_expr_body;
+      typ_strength : module_path option;
+      typ_alias : substitution}
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 544cea246c..03f9be7105 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -181,13 +181,14 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBmodtype of struct_expr_body
+  | SFBalias of module_path * constraints option
+  | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
 
 and struct_expr_body =
   | SEBident of module_path
-  | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body 
+  | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body 
   | SEBstruct of mod_self_id * structure_body
   | SEBapply of struct_expr_body * struct_expr_body
       * constraints
@@ -195,14 +196,16 @@ and struct_expr_body =
 
 and with_declaration_body =
     With_module_body of identifier list * module_path * constraints
-  | With_definition_body of identifier list * constant_body
-
+  | With_definition_body of  identifier list * constant_body
+        
 and module_body = 
     { mod_expr : struct_expr_body option;
       mod_type : struct_expr_body option;
-      mod_equiv : module_path option;
       mod_constraints : constraints;
+      mod_alias : substitution;
       mod_retroknowledge : Retroknowledge.action list}
 
-
-type module_type_body = struct_expr_body * module_path option
+and module_type_body = 
+    { typ_expr : struct_expr_body;
+      typ_strength : module_path option;
+      typ_alias : substitution}
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 89e444a74f..8dde8fb3ed 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -74,6 +74,7 @@ type specification_entry =
     SPEconst of constant_entry
   | SPEmind of mutual_inductive_entry
   | SPEmodule of module_entry
+  | SPEalias of module_path
   | SPEmodtype of module_struct_entry
 
 and module_struct_entry = 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index b757032f89..6de90d29c6 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -73,6 +73,7 @@ type specification_entry =
     SPEconst of constant_entry
   | SPEmind of mutual_inductive_entry
   | SPEmodule of module_entry
+  | SPEalias of module_path
   | SPEmodtype of module_struct_entry
 
 and module_struct_entry = 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 64bb3a6664..13ef7386f0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -287,15 +287,33 @@ let shallow_add_module mp mb env =
 	env_modules = new_mods } in
   { env with env_globals = new_globals }
 
+let rec scrape_alias mp env = 
+  try
+    let mp1 = MPmap.find mp env.env_globals.env_alias in
+      scrape_alias mp1 env
+  with
+      Not_found -> mp
+
 let lookup_module mp env = 
-  MPmap.find mp env.env_globals.env_modules
+  let mp = scrape_alias mp env in
+    MPmap.find mp env.env_globals.env_modules
 
 let lookup_modtype ln env = 
-  MPmap.find ln env.env_globals.env_modtypes
+  let mp = scrape_alias ln env in
+  MPmap.find mp env.env_globals.env_modtypes
+
+let register_alias mp1 mp2 env =
+  let new_alias =  MPmap.add mp1 mp2 env.env_globals.env_alias in
+  let new_globals = 
+    { env.env_globals with 
+	env_alias = new_alias } in
+    { env with env_globals = new_globals }
 
+let lookup_alias mp env =
+  MPmap.find mp env.env_globals.env_alias
 
 (*s Judgments. *)
-
+	
 type unsafe_judgment = { 
   uj_val : constr;
   uj_type : types }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 19c67435c8..c5b4800d56 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -155,6 +155,10 @@ val shallow_add_module : module_path -> module_body -> env -> env
 val lookup_module : module_path -> env -> module_body
 val lookup_modtype : module_path -> env -> module_type_body
 
+val register_alias : module_path -> module_path -> env -> env
+val lookup_alias : module_path -> env -> module_path
+val scrape_alias : module_path -> env -> module_path
+
 (************************************************************************)
 (*s Universe constraints *)
 val set_universes   :   Univ.universes -> env -> env
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index a1e15e3c25..ea477d6a15 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -27,11 +27,15 @@ let apply_opt_resolver resolve kn =
   | Some resolve ->
      try List.assoc kn resolve with Not_found -> None
 
-type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id
+type substitution_domain = 
+    MSI of mod_self_id 
+  | MBI of mod_bound_id
+  | MPI of module_path
 
 let string_of_subst_domain = function
    MSI msid -> debug_string_of_msid msid
  | MBI mbid -> debug_string_of_mbid mbid
+ | MPI mp -> string_of_mp mp
 
 module Umap = Map.Make(struct 
 			 type t = substitution_domain
@@ -46,9 +50,13 @@ let add_msid msid mp =
   Umap.add (MSI msid) (mp,None)
 let add_mbid mbid mp resolve =
   Umap.add (MBI mbid) (mp,resolve)
+let add_mp mp1 mp2  =
+  Umap.add (MPI mp1) (mp2,None)
+
 
 let map_msid msid mp = add_msid msid mp empty_subst
 let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
+let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
 
 let list_contents sub = 
   let one_pair uid (mp,_) l =
@@ -66,6 +74,7 @@ let debug_pr_subst sub =
   in
     str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" 
 
+
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
   match mp with
@@ -74,13 +83,21 @@ let subst_mp0 sub mp = (* 's like subst *)
          mp',resolve
     | MPbound bid ->
         let mp',resolve = Umap.find (MBI bid) sub in
-         mp',resolve
-    | MPdot (mp1,l) -> 
-	let mp1',resolve = aux mp1 in
-	 MPdot (mp1',l),resolve
+          mp',resolve
+    | MPdot (mp1,l) as mp2 ->
+	begin
+	  try  
+	    let mp',resolve = Umap.find (MPI mp2) sub in
+              mp',resolve
+	  with Not_found ->    
+	    let mp1',resolve = aux mp1 in
+	      MPdot (mp1',l),resolve
+	end
     | _ -> raise Not_found
  in
-  try Some (aux mp) with Not_found -> None
+  try
+    Some (aux mp) 
+  with Not_found -> None
 
 let subst_mp sub mp =
  match subst_mp0 sub mp with
@@ -223,60 +240,173 @@ let replace_mp_in_con mpfrom mpto kn =
 exception BothSubstitutionsAreIdentitySubstitutions
 exception ChangeDomain of resolver
 
-let join (subst1 : substitution) (subst2 : substitution) = 
+let join (subst1 : substitution) (subst2 : substitution) =
   let apply_subst (sub : substitution) key (mp,resolve) =
-   let mp',resolve' =
-     match subst_mp0 sub mp with
-	 None -> mp, None
-       | Some (mp',resolve') -> mp',resolve' in
-   let resolve'' : resolver option =
-     try
-       let res =
-	 match resolve with
-             Some res -> res
-	   | None ->
-               match resolve' with
-		   None -> raise BothSubstitutionsAreIdentitySubstitutions
-		 | Some res -> raise (ChangeDomain res)
-       in
-	 Some
-	   (List.map
-              (fun (kn,topt) ->
-		 kn,
-		 match topt with
-		     None ->
-		       (match key with
-			    MSI msid ->
-			      let kn' = replace_mp_in_con (MPself msid) mp kn in
-				apply_opt_resolver resolve' kn'
-			  | MBI mbid ->
-			      let kn' = replace_mp_in_con (MPbound mbid) mp kn in
-				apply_opt_resolver resolve' kn')
-		   | Some t -> Some (subst_mps sub t)) res)
-     with
-	 BothSubstitutionsAreIdentitySubstitutions -> None
-       | ChangeDomain res ->
-	   let rec changeDom = function
-	     | [] -> []
-	     | (kn,topt)::r ->
-		 let key' =
-		   match key with
-                       MSI msid -> MPself msid
-                     | MBI mbid -> MPbound mbid in
-		 let kn' = replace_mp_in_con mp key' kn in
-		   if kn==kn' then
-		     (*the key does not appear in kn, we remove it
-		       from the resolver that we are building*)
-		     changeDom r
-		   else
-		     (kn',topt)::(changeDom r)
-	   in
-	     Some (changeDom res)
-   in
-     mp',resolve'' in
+    let mp',resolve' =
+      match subst_mp0 sub mp with
+	  None -> mp, None
+	| Some (mp',resolve') -> mp',resolve' in
+    let resolve'' : resolver option =
+      try
+	let res =
+	  match resolve with
+              Some res -> res
+	    | None ->
+		match resolve' with
+		    None -> raise BothSubstitutionsAreIdentitySubstitutions
+		  | Some res -> raise (ChangeDomain res)
+	in
+	  Some
+	    (List.map
+               (fun (kn,topt) ->
+		  kn,
+		  match topt with
+		      None ->
+			(match key with
+			     MSI msid ->
+			       let kn' = replace_mp_in_con (MPself msid) mp kn in
+				 apply_opt_resolver resolve' kn'
+			   | MBI mbid ->
+			       let kn' = replace_mp_in_con (MPbound mbid) mp kn in
+				 apply_opt_resolver resolve' kn'
+			   | MPI mp1 ->
+			       let kn' = replace_mp_in_con mp1 mp kn in
+				 apply_opt_resolver resolve' kn')
+		    | Some t -> Some (subst_mps sub t)) res)
+      with
+	  BothSubstitutionsAreIdentitySubstitutions -> None
+	| ChangeDomain res ->
+	    let rec changeDom = function
+	      | [] -> []
+	      | (kn,topt)::r ->
+		  let key' =
+		    match key with
+			MSI msid -> MPself msid
+                      | MBI mbid -> MPbound mbid 
+		      | MPI mp1 -> mp1 in
+		  let kn' = replace_mp_in_con mp key' kn in
+		    if kn==kn' then
+		      (*the key does not appear in kn, we remove it
+			from the resolver that we are building*)
+		      changeDom r
+		    else
+		      (kn',topt)::(changeDom r)
+	    in
+	      Some (changeDom res)
+    in
+      mp',resolve'' in
   let subst = Umap.mapi (apply_subst subst2) subst1 in
-    Umap.fold Umap.add subst2 subst
+    (Umap.fold Umap.add subst2 subst)
       
+let subst_key subst1 subst2 =
+  let replace_in_key key (mp,resolve) sub=
+    let newkey = 
+      match key with
+	| MPI mp1 -> 
+	    begin
+	      match subst_mp0 subst1 mp1 with
+		| None -> None
+		| Some (mp2,_) -> Some (MPI mp2)
+	    end
+	| _ -> None
+    in
+      match newkey with
+	| None -> Umap.add key (mp,resolve) sub
+	| Some mpi -> Umap.add mpi (mp,resolve) sub
+  in
+    Umap.fold replace_in_key subst2 empty_subst
+
+let update_subst_alias subst1 subst2 =
+ let subst_inv key (mp,resolve) sub =
+    let newmp = 
+      match key with 
+	| MBI msid -> Some (MPbound msid)
+	| MSI msid -> Some (MPself msid)
+	| _ -> None
+    in
+      match newmp with
+	| None -> sub
+	| Some mpi -> match mp with 
+	    | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub
+	    | MPself msid -> Umap.add (MSI msid) (mpi,None) sub
+	    | _ ->  Umap.add (MPI mp) (mpi,None) sub
+  in 
+  let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
+  let alias_subst key (mp,resolve) sub=
+    let newkey = 
+      match key with
+	| MPI mp1 -> 
+	    begin
+	      match subst_mp0 subst_mbi mp1 with
+		| None -> None
+		| Some (mp2,_) -> Some (MPI mp2)
+	    end
+	| _ -> None
+    in
+      match newkey with
+	| None -> Umap.add key (mp,resolve) sub
+	| Some mpi -> Umap.add mpi (mp,resolve) sub
+  in
+    Umap.fold alias_subst subst1 empty_subst
+
+let join_alias (subst1 : substitution) (subst2 : substitution) =
+  let apply_subst (sub : substitution) key (mp,resolve) =
+    let mp',resolve' =
+      match subst_mp0 sub mp with
+	  None -> mp, None
+	| Some (mp',resolve') -> mp',resolve' in
+    let resolve'' : resolver option =
+      try
+	let res =
+	  match resolve with
+              Some res -> res
+	    | None ->
+		match resolve' with
+		    None -> raise BothSubstitutionsAreIdentitySubstitutions
+		  | Some res -> raise (ChangeDomain res)
+	in
+	  Some
+	    (List.map
+               (fun (kn,topt) ->
+		  kn,
+		  match topt with
+		      None ->
+			(match key with
+			     MSI msid ->
+			       let kn' = replace_mp_in_con (MPself msid) mp kn in
+				 apply_opt_resolver resolve' kn'
+			   | MBI mbid ->
+			       let kn' = replace_mp_in_con (MPbound mbid) mp kn in
+				 apply_opt_resolver resolve' kn'
+			   | MPI mp1 ->
+			       let kn' = replace_mp_in_con mp1 mp kn in
+				 apply_opt_resolver resolve' kn')
+		    | Some t -> Some (subst_mps sub t)) res)
+      with
+	  BothSubstitutionsAreIdentitySubstitutions -> None
+	| ChangeDomain res ->
+	    let rec changeDom = function
+	      | [] -> []
+	      | (kn,topt)::r ->
+		  let key' =
+		    match key with
+			MSI msid -> MPself msid
+                      | MBI mbid -> MPbound mbid 
+		      | MPI mp1 -> mp1 in
+		  let kn' = replace_mp_in_con mp key' kn in
+		    if kn==kn' then
+		      (*the key does not appear in kn, we remove it
+			from the resolver that we are building*)
+		      changeDom r
+		    else
+		      (kn',topt)::(changeDom r)
+	    in
+	      Some (changeDom res)
+    in
+      mp',resolve'' in
+  Umap.mapi (apply_subst subst2) subst1 
+
+
 let rec occur_in_path uid path =
  match uid,path with
   | MSI sid,MPself sid' -> sid = sid'
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 0a3220293b..b54ae6f3b4 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -24,11 +24,15 @@ val add_msid :
   mod_self_id -> module_path -> substitution -> substitution
 val add_mbid : 
   mod_bound_id -> module_path -> resolver option -> substitution -> substitution
+val add_mp :
+  module_path -> module_path -> substitution -> substitution
 
 val map_msid :
   mod_self_id -> module_path -> substitution
 val map_mbid :
   mod_bound_id -> module_path -> resolver option -> substitution
+val map_mp :
+  module_path -> module_path -> substitution
 
 (* sequential composition: 
    [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
@@ -78,3 +82,9 @@ val subst_mps : substitution -> constr -> constr
 
 val occur_msid : mod_self_id -> substitution -> bool
 val occur_mbid : mod_bound_id -> substitution -> bool
+
+val update_subst_alias : substitution -> substitution -> substitution
+
+val subst_key : substitution -> substitution -> substitution
+
+val join_alias : substitution -> substitution -> substitution
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 201835c101..3ae9293c73 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -22,7 +22,7 @@ open Mod_subst
 exception Not_path
 
 let path_of_mexpr = function
-  | MSEident mb -> mb
+  | MSEident mp -> mp
   | _ -> raise Not_path
 
 let rec list_split_assoc k rev_before = function
@@ -41,10 +41,10 @@ let rec check_with env mtb with_decl =
   match with_decl with
     | With_Definition (id,_) -> 
 	let cb = check_with_aux_def env mtb with_decl in
-	  SEBwith(mtb,With_definition_body(id,cb))
+	  SEBwith(mtb,With_definition_body(id,cb)),empty_subst
     | With_Module (id,mp) -> 
-	let cst = check_with_aux_mod env mtb with_decl in
-	  SEBwith(mtb,With_module_body(id,mp,cst))
+	let cst,sub = check_with_aux_mod env mtb with_decl in
+	  SEBwith(mtb,With_module_body(id,mp,cst)),sub
 
 and check_with_aux_def env mtb with_decl = 
   let msid,sig_b = match (eval_struct env mtb) with 
@@ -102,13 +102,13 @@ and check_with_aux_def env mtb with_decl =
 		| _ -> error_not_a_module (string_of_label l)
 	      in
 		begin
-		  match old.mod_equiv with
+		  match old.mod_expr with
                     | None ->
 			let new_with_decl = match with_decl with
 			    With_Definition (_,c) -> With_Definition (idl,c)
 			  | With_Module (_,c) -> With_Module (idl,c) in 
 			  check_with_aux_def env' (type_of_mb env old) new_with_decl
-                    | Some mp ->
+                    | Some msb ->
 			error_a_generative_module_expected l
 		end
 	  | _ -> anomaly "Modtyping:incorrect use of with"
@@ -117,9 +117,9 @@ and check_with_aux_def env mtb with_decl =
       | Reduction.NotConvertible -> error_with_incorrect l
 
 and check_with_aux_mod env mtb with_decl = 
-  let msid,sig_b = match (eval_struct env mtb) with 
+  let initmsid,msid,sig_b = match (eval_struct env mtb) with 
     | SEBstruct(msid,sig_b) ->let msid'=(refresh_msid msid) in
-	msid',(subst_signature_msid msid (MPself(msid')) sig_b)
+	msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
     | _ -> error_signature_expected mtb
   in
   let id,idl = match with_decl with 
@@ -130,39 +130,56 @@ and check_with_aux_mod env mtb with_decl =
     try
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
+      let rec mp_rec = function
+	| [] -> MPself initmsid
+	| i::r -> MPdot(mp_rec r,label_of_id i)
+      in 
       let env' = Modops.add_signature (MPself msid) before env in
 	match with_decl with
           | With_Module ([],_) -> assert false
 	  | With_Module ([id], mp) ->
-	      let old = match spec with
-		  SFBmodule msb -> msb
+	      let old,alias = match spec with
+		  SFBmodule msb -> Some msb,None
+		| SFBalias (mp',cst) -> None,Some (mp',cst)
 		| _ -> error_not_a_module (string_of_label l)
 	      in
-	      let mtb' = eval_struct env' (SEBident mp) in
+	      let mtb' = lookup_modtype mp env' in
 	      let cst =
-		try check_subtypes env' mtb' (type_of_mb env old)
-              with Failure _ -> error_with_incorrect (label_of_id id) in
-	      let _ = 
- 		match old.mod_equiv with
-		| None -> Some mp
-		| Some mp' -> 
-		    check_modpath_equiv env' mp mp';
-		    Some mp
+		match old,alias with
+		    Some msb,None ->
+		      begin
+			try Constraint.union 
+			  (check_subtypes env' mtb' (module_type_of_module None msb))
+			  msb.mod_constraints
+			with Failure _ -> error_with_incorrect (label_of_id id)
+		      end
+		  | None,Some (mp',None) ->
+		      check_modpath_equiv env' mp mp';
+		      Constraint.empty
+		  | None,Some (mp',Some cst) ->
+		      check_modpath_equiv env' mp mp';
+		      cst
+		  | _,_ ->
+		      anomaly "Mod_typing:no implementation and no alias"
 	      in
-		cst
-        | With_Module (_::_,_) -> 
+		cst,join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
+        | With_Module (_::_,mp) -> 
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
 	      begin
-		match old.mod_equiv with
+		match old.mod_expr with
                     None ->
                       let new_with_decl = match with_decl with
-			  With_Definition (_,c) -> With_Definition (idl,c)
+			  With_Definition (_,c) -> 
+			    With_Definition (idl,c)
 			| With_Module (_,c) -> With_Module (idl,c) in
-			check_with_aux_mod env' (type_of_mb env old) new_with_decl 
-                  | Some mp ->
+		      let cst,sub =
+			check_with_aux_mod env' 
+			  (type_of_mb env old) new_with_decl in
+			cst,(join (map_mp (mp_rec idl) mp) sub)
+                  | Some msb ->
                       error_a_generative_module_expected l
               end
 	| _ -> anomaly "Modtyping:incorrect use of with"
@@ -175,35 +192,33 @@ and translate_module env me =
     | None, None -> 
 	anomaly "Mod_typing.translate_module: empty type and expr in module entry"
     | None, Some mte -> 
-	let mtb = translate_struct_entry env mte in
+	let mtb,sub = translate_struct_entry env mte in
 	{ mod_expr = None;
 	  mod_type = Some mtb;
-	  mod_equiv = None;
+	  mod_alias = sub;
 	  mod_constraints = Constraint.empty; 
 	  mod_retroknowledge = []}
     | Some mexpr, _ -> 
-	let meq_o = 
-	  try       (* TODO: transparent field in module_entry *)
-	    match me.mod_entry_type with
-	      | None -> Some (path_of_mexpr mexpr)
-	      | Some _ -> None
-	  with 
-	    | Not_path -> None
-	in
-	let meb = translate_struct_entry env mexpr in
-	let mod_typ, cst =
+	let meb,sub1 = translate_struct_entry env mexpr in
+	let mod_typ,sub,cst =
 	  match me.mod_entry_type with
-	    | None ->  None, Constraint.empty
+	    | None ->  None,sub1,Constraint.empty
 	    | Some mte -> 
-		let mtb1 = translate_struct_entry env mte in
-                let cst = check_subtypes env (eval_struct env meb)
-		  mtb1 in
-		  Some mtb1, cst
+		let mtb2,sub2 = translate_struct_entry env mte in
+                let cst = check_subtypes env
+		  {typ_expr = meb;
+		   typ_strength = None;
+		   typ_alias = sub1;}
+		  {typ_expr = mtb2;
+		   typ_strength = None;
+		   typ_alias = sub2;}
+		in
+		  Some mtb2,sub2,cst
 	in
 	  { mod_type = mod_typ;
 	    mod_expr = Some meb;
-	    mod_equiv = meq_o;
 	    mod_constraints = cst;
+	    mod_alias = sub;
 	    mod_retroknowledge = []} (* spiwack: not so sure about that. It may
 					cause a bug when closing nested modules.
 					If it does, I don't really know how to
@@ -211,31 +226,39 @@ and translate_module env me =
 
 
 and translate_struct_entry env mse = match mse with
-  | MSEident mp -> 
-      SEBident mp
+  | MSEident mp ->
+      let mtb = lookup_modtype mp env in 
+      SEBident mp,mtb.typ_alias
   | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let arg_b = translate_struct_entry env arg_e in
-      let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in
-      let body_b = translate_struct_entry env' body_expr in
-	SEBfunctor (arg_id, arg_b, body_b)
+      let arg_b,sub = translate_struct_entry env arg_e in
+      let mtb =
+	{typ_expr = arg_b;
+	 typ_strength = None;
+	 typ_alias = sub} in
+      let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in
+      let body_b,sub = translate_struct_entry env' body_expr in
+	SEBfunctor (arg_id, mtb, body_b),sub
   | MSEapply (fexpr,mexpr) ->
-      let feb = translate_struct_entry env fexpr in
+      let feb,sub1 = translate_struct_entry env fexpr in
       let feb'= eval_struct env feb
       in
       let farg_id, farg_b, fbody_b = destr_functor env feb' in
-      let _ = 
+      let mtb = 
 	try
-	  path_of_mexpr mexpr 
+	  lookup_modtype (path_of_mexpr mexpr) env
 	with
 	  | Not_path -> error_application_to_not_path mexpr
 	      (* place for nondep_supertype *) in
-      let meb= translate_struct_entry env mexpr in
-      let cst = check_subtypes env (eval_struct env meb) farg_b in
-	SEBapply(feb,meb,cst)
+      let meb,sub2= translate_struct_entry env mexpr in
+      let sub = join sub1 sub2 in
+      let sub = join_alias sub (map_mbid farg_id (path_of_mexpr mexpr) None) in
+      let sub = update_subst_alias sub (map_mbid farg_id (path_of_mexpr mexpr) None) in
+      let cst = check_subtypes env mtb farg_b in
+	SEBapply(feb,meb,cst),sub
   | MSEwith(mte, with_decl) ->
-	let mtb = translate_struct_entry env mte in
-	let mtb' = check_with env mtb with_decl in
-	  mtb'
+	let mtb,sub1 = translate_struct_entry env mte in
+	let mtb',sub2 = check_with env mtb with_decl in
+	  mtb',join sub1 sub2
 
 
 let rec add_struct_expr_constraints env = function
@@ -267,6 +290,8 @@ and add_struct_elem_constraints env = function
   | SFBconst cb -> Environ.add_constraints cb.const_constraints env
   | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
   | SFBmodule mb -> add_module_constraints env mb
+  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
+  | SFBalias (mp,None) -> env
   | SFBmodtype mtb -> add_modtype_constraints env mtb
 
 and add_module_constraints env mb = 
@@ -277,10 +302,10 @@ and add_module_constraints env mb =
   let env = match mb.mod_type with
     | None -> env
     | Some mtb -> 
-	add_modtype_constraints env mtb
+	add_struct_expr_constraints env mtb
   in
     Environ.add_constraints mb.mod_constraints env
 
 and add_modtype_constraints env mtb = 
-  add_struct_expr_constraints env mtb
+  add_struct_expr_constraints env mtb.typ_expr
       
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 124cb89c4d..e3045555f5 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -12,16 +12,18 @@
 open Declarations
 open Environ
 open Entries
+open Mod_subst
 (*i*)
 
 
 val translate_module : env -> module_entry -> module_body
 
-val translate_struct_entry : env -> module_struct_entry -> struct_expr_body
+val translate_struct_entry : env -> module_struct_entry -> 
+  struct_expr_body * substitution
 
-val add_modtype_constraints : env -> struct_expr_body -> env
+val add_modtype_constraints : env -> module_type_body -> env
 
 val add_module_constraints : env -> module_body -> env
 
-
+val add_struct_expr_constraints : env -> struct_expr_body -> env
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index c5b8e15b50..dc339af52e 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -93,7 +93,7 @@ let rec list_split_assoc k rev_before = function
   | h::tail -> list_split_assoc k (h::rev_before) tail
 
 let path_of_seb = function
-  | SEBident mb -> mb
+  | SEBident mp -> mp
   | _ -> anomaly "Modops: evaluation failed."
 
 
@@ -106,24 +106,32 @@ let destr_functor env mtb =
 (* the constraints are not important here *)
 
 let module_body_of_type mtb = 
-  { mod_type = Some mtb;
-    mod_equiv = None;
+  { mod_type = Some mtb.typ_expr;
     mod_expr = None;
     mod_constraints = Constraint.empty;
+    mod_alias = mtb.typ_alias;
     mod_retroknowledge = []}
 
+let module_type_of_module mp mb =
+  {typ_expr = 
+      (match mb.mod_type with
+	| Some expr -> expr
+	| None -> (match mb.mod_expr with
+		     | Some expr -> expr
+		     | None -> 
+			 anomaly "Modops: empty expr and type"));
+   typ_alias = mb.mod_alias;
+   typ_strength = mp
+  }
 
 let rec check_modpath_equiv env mp1 mp2 = 
   if mp1=mp2 then () else
-  let mb1 = lookup_module mp1 env in
-    match mb1.mod_equiv with
-      | None ->
-	  let mb2 = lookup_module mp2 env in
-	    (match mb2.mod_equiv with
-	      | None -> error_not_equal mp1 mp2
-	      | Some mp2' -> check_modpath_equiv env mp2' mp1)
-      | Some mp1' -> check_modpath_equiv env mp2 mp1'
-
+  let mp1 = scrape_alias mp1 env in
+  let mp2 = scrape_alias mp2 env in
+    if mp1=mp2 then ()
+    else 
+      error_not_equal mp1 mp2
+	
 let subst_with_body sub = function
   | With_module_body(id,mp,cst) ->
       With_module_body(id,subst_mp sub mp,cst)
@@ -131,8 +139,13 @@ let subst_with_body sub = function
       With_definition_body( id,subst_const_body sub cb)
 
 let rec subst_modtype sub mtb =
-  subst_struct_expr sub mtb
-  
+  let typ_expr' = subst_struct_expr sub mtb.typ_expr in
+    if typ_expr'==mtb.typ_expr then
+      mtb
+    else
+      { mtb with 
+	  typ_expr = typ_expr'}
+	
 and subst_structure sub sign = 
   let subst_body  = function
       SFBconst cb -> 
@@ -143,23 +156,26 @@ and subst_structure sub sign =
 	SFBmodule (subst_module sub mb)
     | SFBmodtype mtb -> 
 	SFBmodtype (subst_modtype sub mtb)
+    | SFBalias (mp,cst) ->
+	SFBalias (subst_mp sub mp,cst)
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
 and subst_module  sub mb =
-  let mtb' = Option.smartmap (subst_modtype sub) mb.mod_type in
+  let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in
   (* This is similar to the previous case. In this case we have
      a module M in a signature that is knows to be equivalent to a module M'
      (because the signature is "K with Module M := M'") and we are substituting
      M' with some M''. *)
   let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in
-  let mpo' = Option.smartmap (subst_mp sub) mb.mod_equiv in
-    if mtb'==mb.mod_type && mpo'==mb.mod_equiv && mb.mod_expr == me' 
+  let mb_alias = join_alias mb.mod_alias sub in
+    if mtb'==mb.mod_type && mb.mod_expr == me' 
+      && mb_alias == mb.mod_alias
     then mb else
       { mod_expr = me';
 	mod_type=mtb'; 
-	mod_equiv=mpo'; 
 	mod_constraints=mb.mod_constraints;
+	mod_alias = mb_alias;
 	mod_retroknowledge=mb.mod_retroknowledge}
 
 
@@ -230,7 +246,8 @@ let strengthen_mind env mp l mib = match mib.mind_equiv with
 let rec eval_struct env = function 
   | SEBident mp -> 
       begin
-	match (lookup_modtype mp env) with
+	let mtb =lookup_modtype mp env in
+	match mtb.typ_expr,mtb.typ_strength with
 	    mtb,None -> eval_struct env mtb
 	  | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb)
       end
@@ -238,10 +255,26 @@ let rec eval_struct env = function
       let svb1 = eval_struct env seb1 in
       let farg_id, farg_b, fbody_b = destr_functor env svb1 in
       let mp = path_of_seb seb2 in
-      let resolve = resolver_of_environment farg_id farg_b mp env in
-	eval_struct env (subst_modtype 
-			   (map_mbid farg_id mp (Some resolve)) fbody_b)
-  | SEBwith (mtb,wdb) -> merge_with env mtb wdb
+      let mp = scrape_alias mp env in
+      let sub_alias = (lookup_modtype mp env).typ_alias in
+      let sub_alias = match eval_struct env (SEBident mp) with
+	  | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias
+	  | _ -> sub_alias in
+      let sub_alias = update_subst_alias sub_alias 
+	(map_mbid farg_id mp (None)) in
+      let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in
+	eval_struct env (subst_struct_expr 
+			   (join sub_alias 
+			      (map_mbid farg_id mp (Some resolve))) fbody_b)
+  | SEBwith (mtb,(With_definition_body _ as wdb)) ->
+      merge_with env mtb wdb empty_subst
+  | SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) ->
+      let alias_in_mp =
+	(lookup_modtype mp env).typ_alias in
+	merge_with env mtb wdb alias_in_mp
+(*  | SEBfunctor(mbid,mtb,body) -> 
+      let env = add_module (MPbound mbid) (module_body_of_type mtb) env in
+	SEBfunctor(mbid,mtb,eval_struct env body) *)
   | mtb -> mtb
       
 and type_of_mb env mb =
@@ -251,7 +284,7 @@ and type_of_mb env mb =
     | _,_ -> anomaly 
 	"Modops:  empty type and empty expr" 
 	  
-and merge_with env mtb with_decl = 
+and merge_with env mtb with_decl alias= 
   let msid,sig_b = match (eval_struct env mtb) with 
     | SEBstruct(msid,sig_b) -> msid,sig_b
     | _ -> error_signature_expected mtb
@@ -264,50 +297,50 @@ and merge_with env mtb with_decl =
     try
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
-      let new_spec = match with_decl with
+      let rec mp_rec = function
+	| [] -> MPself msid
+	| i::r -> MPdot(mp_rec r,label_of_id i)
+      in 
+      let new_spec,subst = match with_decl with
         | With_definition_body ([],_)
         | With_module_body ([],_,_) -> assert false
 	| With_definition_body ([id],c) -> 
-	    SFBconst c
+	    SFBconst c,None
 	| With_module_body ([id], mp,cst) ->
-	    let old = match spec with
-		SFBmodule msb -> msb
-	      | _ -> error_not_a_module (string_of_label l)
-	    in
-	    let mtb' = eval_struct env (SEBident mp) in
-	    let msb =
-	      {mod_expr = Some (SEBident mp);
-	       mod_type = Some mtb'; 
-	       mod_equiv = Some mp; 
-	       mod_constraints = cst;
-	       mod_retroknowledge = old.mod_retroknowledge }
-	    in
-	      (SFBmodule msb)
+	    let mp' = scrape_alias mp env in
+	      SFBalias (mp,Some cst),
+	    Some(join (map_mp (mp_rec [id]) mp') alias)
 	| With_definition_body (_::_,_) 
         | With_module_body (_::_,_,_) -> 
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
-            let new_with_decl = match with_decl with
-                With_definition_body (_,c) -> With_definition_body (idl,c)
-              | With_module_body (_,c,cst) -> With_module_body (idl,c,cst) in
+            let new_with_decl,subst1 = 
+	      match with_decl with
+                  With_definition_body (_,c) -> With_definition_body (idl,c),None
+		| With_module_body (idc,mp,cst) -> 
+		    With_module_body (idl,mp,cst),
+		      Some(map_mp (mp_rec idc) mp) 
+	    in
+	    let subst = Option.fold_right join subst1 alias in
             let modtype = 
-              merge_with env (type_of_mb env old) new_with_decl in
-                    let msb =
-		      { mod_expr = None;
-			mod_type = Some modtype; 
-			mod_equiv = None; 
-			mod_constraints = old.mod_constraints;
-			mod_retroknowledge = old.mod_retroknowledge}
-	            in
-	             (SFBmodule msb)
+              merge_with env (type_of_mb env old) new_with_decl alias in
+            let msb =
+	      { mod_expr = None;
+		mod_type = Some modtype; 
+		mod_constraints = old.mod_constraints;
+		mod_alias = subst;
+		mod_retroknowledge = old.mod_retroknowledge}
+	    in
+	      (SFBmodule msb),Some subst
       in
-	SEBstruct(msid,  before@(l,new_spec)::after)
+	SEBstruct(msid,  before@(l,new_spec)::
+		    (Option.fold_right subst_structure subst after))
     with
 	Not_found -> error_no_such_label l
 
-and  add_signature mp sign env = 
+and add_signature mp sign env = 
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
     let con = make_con mp empty_dirpath l in
@@ -316,20 +349,19 @@ and  add_signature mp sign env =
 	| SFBmind mib -> Environ.add_mind kn mib env
 	| SFBmodule mb -> 
 	    add_module (MPdot (mp,l)) mb env 
-	    (* adds components as well *)
+	      (* adds components as well *)
+	| SFBalias (mp1,cst) -> 
+	    Environ.register_alias (MPdot(mp,l)) mp1 env
 	| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) 
-	    (mtb,None) env
+	    mtb env
   in
     List.fold_left add_one env sign
 
 and add_module mp mb env = 
   let env = Environ.shallow_add_module mp mb env in
-  let env = match mb.mod_type,mb.mod_expr with
-    | Some mt, _ -> 
-	Environ.add_modtype mp (mt,Some mp) env
-    | None, Some me -> 
-	Environ.add_modtype mp (me,Some mp) env 
-    | _,_ -> anomaly "Modops:Empty expr and type" in
+  let env =
+    Environ.add_modtype mp (module_type_of_module (Some mp) mb) env
+  in
   let mod_typ = type_of_mb env mb in
     match mod_typ with
       | SEBstruct (msid,sign) -> 
@@ -346,9 +378,13 @@ and  constants_of_specification env mp sign =
    | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
    | SFBmind _ -> env,res
    | SFBmodule mb ->
-       let new_env =  add_module (MPdot (mp,l))  mb env in 
+       let new_env =  add_module (MPdot (mp,l)) mb env in 
        new_env,(constants_of_modtype env (MPdot (mp,l))
 		   (type_of_mb env mb)) @ res
+   | SFBalias (mp1,cst) ->
+       let new_env =  register_alias (MPdot (mp,l)) mp1 env in 
+       new_env,(constants_of_modtype env (MPdot (mp,l))
+		   (eval_struct env (SEBident mp1))) @ res
    | SFBmodtype mtb -> 
        (* module type dans un module type. 
 	  Il faut au moins mettre mtb dans l'environnement (avec le bon 
@@ -365,27 +401,29 @@ and  constants_of_specification env mp sign =
 	  si on ne rajoute pas T2 dans l'environement de typage 
 	  on va exploser au moment du Declare Module
        *)
-       let new_env = Environ.add_modtype (MPdot(mp,l)) (mtb,None) env in 
-       new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res
+       let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in 
+       new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res
  in
  snd (List.fold_left aux (env,[]) sign)
 
 and constants_of_modtype env mp modtype =
- match (eval_struct env modtype) with
-     SEBstruct (msid,sign) ->
-       constants_of_specification env mp
-	 (subst_signature_msid msid mp sign)
-   | SEBfunctor _ -> []
-   | _ -> anomaly "Modops:the evaluation of the structure failed "
+  match (eval_struct env modtype) with
+      SEBstruct (msid,sign) ->
+	constants_of_specification env mp
+	  (subst_signature_msid msid mp sign)
+    | SEBfunctor _ -> []
+    | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 (* returns a resolver for kn that maps mbid to mp. We only keep
    constants that have the inline flag *)
-and  resolver_of_environment mbid modtype mp env =
- let constants = constants_of_modtype env (MPbound mbid) modtype in
+and  resolver_of_environment mbid modtype mp alias env =
+ let constants = constants_of_modtype env (MPbound mbid) modtype.typ_expr in
+ let constants = List.map (fun (l,cb) -> (l,subst_const_body alias cb)) constants in
  let rec make_resolve = function
    | [] -> []
    | (con,expecteddef)::r ->
-       let con' = replace_mp_in_con (MPbound mbid) mp con in
+       let con',_ = subst_con alias con in
+       let con' = replace_mp_in_con (MPbound mbid) mp con' in
 	 try
 	   if expecteddef.Declarations.const_inline then
 	     let constant = lookup_constant con' env in
@@ -413,11 +451,8 @@ and strengthen_mod env mp mb =
   let mod_typ = type_of_mb env mb in
     { mod_expr = mb.mod_expr;
       mod_type = Some (strengthen_mtb env mp mod_typ);
-      mod_equiv = begin match mb.mod_equiv with
-	| Some _ -> mb.mod_equiv
-	| None -> Some mp 
-      end ;
       mod_constraints = mb.mod_constraints;
+      mod_alias = mb.mod_alias;
       mod_retroknowledge = mb.mod_retroknowledge}
       
 and strengthen_sig env msid sign mp = match sign with
@@ -432,18 +467,19 @@ and strengthen_sig env msid sign mp = match sign with
 	item'::rest'
   | (l,SFBmodule mb) :: rest ->
       let mp' = MPdot (mp,l) in
-      let item' = l,SFBmodule (strengthen_mod env mp' mb) in
-      let env' = add_module 
-		   (MPdot (MPself msid,l)) 
-		   mb 
-		   env 
-      in
+	let item' = l,SFBmodule (strengthen_mod env mp' mb) in
+	let env' = add_module 
+	  (MPdot (MPself msid,l)) mb env in
+        let rest' = strengthen_sig env' msid rest mp in
+	item':: rest'
+  | ((l,SFBalias (mp1,cst)) as item) :: rest ->
+      let env' = register_alias (MPdot(MPself msid,l)) mp1 env in
       let rest' = strengthen_sig env' msid rest mp in
-	item'::rest'
+	item::rest'
   | (l,SFBmodtype mty as item) :: rest -> 
       let env' = add_modtype 
 		   (MPdot((MPself msid),l)) 
-		   (mty,None)
+		   mty
 		   env
       in
       let rest' = strengthen_sig env' msid rest mp in
@@ -451,5 +487,11 @@ and strengthen_sig env msid sign mp = match sign with
 
     
 let strengthen env mtb mp = strengthen_mtb env mp mtb
-  
 
+
+let update_subst env mb mp =
+  match type_of_mb env mb with
+    | SEBstruct(msid,str) -> false, join_alias 
+	(subst_key (map_msid msid mp) mb.mod_alias)
+	(map_msid msid mp)
+    | _ -> true, mb.mod_alias
diff --git a/kernel/modops.mli b/kernel/modops.mli
index a35e887ea3..11f0ddd171 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -21,19 +21,25 @@ open Mod_subst
 (* Various operations on modules and module types *)
 
 (* make the environment entry out of type *)
-val module_body_of_type : struct_expr_body -> module_body
+val module_body_of_type : module_type_body -> module_body
 
+val  module_type_of_module : module_path option -> module_body -> 
+  module_type_body 
 
 val destr_functor : 
-  env -> struct_expr_body -> mod_bound_id * struct_expr_body * struct_expr_body
+  env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body
 
-val subst_modtype : substitution -> struct_expr_body -> struct_expr_body
+val subst_modtype : substitution -> module_type_body -> module_type_body
 val subst_structure : substitution -> structure_body -> structure_body
 
+val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
+
 val subst_signature_msid :
   mod_self_id -> module_path -> 
   structure_body -> structure_body
 
+val subst_structure : substitution -> structure_body -> structure_body
+
 (* Evaluation functions *)
 val eval_struct : env -> struct_expr_body -> struct_expr_body
 
@@ -53,6 +59,8 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit
 
 val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body
 
+val update_subst : env -> module_body -> module_path -> bool * substitution
+
 val error_existing_label : label -> 'a
 
 val error_declaration_not_path : module_struct_entry -> 'a
@@ -62,7 +70,7 @@ val error_application_to_not_path : module_struct_entry -> 'a
 val error_not_a_functor :  module_struct_entry -> 'a
 
 val error_incompatible_modtypes : 
-    struct_expr_body -> struct_expr_body -> 'a
+  module_type_body -> module_type_body -> 'a
 
 val error_not_equal : module_path -> module_path -> 'a
 
@@ -97,4 +105,6 @@ val error_local_context : label option -> 'a
 val error_no_such_label_sub : label->string->string->'a
 
 val resolver_of_environment :
-  mod_bound_id -> struct_expr_body -> module_path -> env -> resolver
+  mod_bound_id -> module_type_body -> module_path -> substitution 
+  -> env -> resolver
+
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 2b41e5a363..8d45bb9e3d 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -26,7 +26,8 @@ type globals = {
   env_constants : constant_key Cmap.t;
   env_inductives : mutual_inductive_body KNmap.t;
   env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t }
+  env_modtypes : module_type_body MPmap.t;
+  env_alias : module_path MPmap.t }
 
 type stratification = {
   env_universes : universes;
@@ -60,7 +61,8 @@ let empty_env = {
     env_constants = Cmap.empty;
     env_inductives = KNmap.empty;
     env_modules = MPmap.empty;
-    env_modtypes = MPmap.empty };
+    env_modtypes = MPmap.empty;
+    env_alias = MPmap.empty };
   env_named_context = empty_named_context;
   env_named_vals = [];
   env_rel_context = empty_rel_context;
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index b6d83b918c..518c6330d8 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -26,7 +26,8 @@ type globals = {
   env_constants : constant_key Cmap.t;
   env_inductives : mutual_inductive_body KNmap.t;
   env_modules : module_body MPmap.t;
-  env_modtypes : module_type_body MPmap.t }
+  env_modtypes : module_type_body MPmap.t;
+  env_alias : module_path MPmap.t }
 
 type stratification = {
   env_universes : universes;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 28e6fb8c72..b1eea3bbdb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -25,11 +25,12 @@ open Term_typing
 open Modops
 open Subtyping
 open Mod_typing
+open Mod_subst
 
 type modvariant = 
   | NONE 
-  | SIG of (* funsig params *) (mod_bound_id * struct_expr_body) list 
-  | STRUCT of (* functor params *) (mod_bound_id * struct_expr_body) list
+  | SIG of (* funsig params *) (mod_bound_id * module_type_body) list 
+  | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
   | LIBRARY of dir_path
 
 type module_info = 
@@ -37,7 +38,8 @@ type module_info =
       modpath : module_path;
       seed : dir_path; (* the "seed" of unique identifier generator *)
       label : label;
-      variant : modvariant}
+      variant : modvariant;
+      alias_subst : substitution}
 
 let check_label l labset = 
   if Labset.mem l labset then error_existing_label l
@@ -81,7 +83,8 @@ let rec empty_environment =
       modpath = initial_path;
       seed = initial_dir;
       label = mk_label "_";
-      variant = NONE};
+      variant = NONE;
+      alias_subst = empty_subst};
     labset = Labset.empty;
     revstruct = [];
     univ = Univ.Constraint.empty;
@@ -253,10 +256,13 @@ let add_mind dir l mie senv =
 
 let add_modtype l mte senv = 
   check_label l senv.labset; 
-  let mtb = translate_struct_entry senv.env mte  in
+  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 env' = add_modtype_constraints senv.env mtb in
   let mp = MPdot(senv.modinfo.modpath, l) in
-  let env'' = Environ.add_modtype mp (mtb,None) env' in
+  let env'' = Environ.add_modtype mp mtb env' in
   mp, { old = senv.old;
 	env = env'';
 	modinfo = senv.modinfo;
@@ -281,10 +287,16 @@ 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 is_functor,sub = Modops.update_subst senv.env mb mp in
   let env' = full_add_module mp mb senv.env in
   mp, { old = senv.old;
 	env = env';
-	modinfo = senv.modinfo;
+	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;
@@ -293,6 +305,26 @@ let add_module l me senv =
 	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
+  (* we get all alias substitutions that comes from mp *)
+  let _,sub = translate_struct_entry senv.env (MSEident mp) in
+   (* we add the new one *)
+  let sub = join (map_mp mp' mp) 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,None))::senv.revstruct;
+        univ = senv.univ;
+        engagement = senv.engagement;
+	imports = senv.imports;
+	loads = senv.loads;
+        local_retroknowledge = senv.local_retroknowledge }
 
 (* Interactive modules *)
 
@@ -304,7 +336,8 @@ let start_module l senv =
 		  modpath = mp;
 		  seed = senv.modinfo.seed;
 		  label = l;
-		  variant = STRUCT [] }
+		  variant = STRUCT [];
+		  alias_subst = empty_subst}
   in
   mp, { old = senv;
 	env = senv.env;
@@ -322,10 +355,10 @@ 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 params = 
+  let params,is_functor = 
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
-      | STRUCT params -> params
+      | STRUCT params -> params, (List.length params > 0)
   in
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_local_context None;
@@ -339,21 +372,27 @@ let end_module l restype senv =
    let auto_tb = 
      SEBstruct (modinfo.msid, List.rev senv.revstruct)
   in
-  let mod_typ, cst = 
+  let mod_typ,subst,cst = 
     match restype with
-      | None ->  None, Constraint.empty
-      | Some res_tb -> 
-	  let cst = check_subtypes senv.env auto_tb res_tb in
+      | 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, cst
+	    Some mtb,subst,cst
   in
   let mexpr = functorize_struct auto_tb in
   let cst = Constraint.union cst senv.univ in
   let mb = 
     { mod_expr = Some mexpr;
       mod_type = mod_typ;
-      mod_equiv = None;
       mod_constraints = cst;
+      mod_alias = subst;
       mod_retroknowledge = senv.local_retroknowledge }
   in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
@@ -368,9 +407,19 @@ let end_module l restype senv =
   let newenv = 
     full_add_module mp mb newenv
   in 
-  mp, { old = oldsenv.old;
+  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 };
+  in
+    mp, { old = oldsenv.old;
 	env = newenv;
-	modinfo = oldsenv.modinfo;
+	modinfo = newmodinfo;
 	labset = Labset.add l oldsenv.labset;
 	revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
         univ = oldsenv.univ;
@@ -383,8 +432,8 @@ let end_module l restype senv =
 
 (* Include for module and module type*)
  let add_include me senv =
-   let struct_expr =  translate_struct_entry senv.env me in
-   let senv = { senv with env = add_modtype_constraints senv.env struct_expr } in
+   let struct_expr,_ =  translate_struct_entry senv.env me in
+   let senv = { senv with env = add_struct_expr_constraints senv.env struct_expr } 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" )
@@ -426,21 +475,42 @@ let end_module l restype senv =
 	       
        | SFBmodule mb ->
 	   let mp = MPdot(senv.modinfo.modpath, l) in
+	   let is_functor,sub = Modops.update_subst senv.env mb mp in
 	   let env' = full_add_module mp mb senv.env in
 	     { old = senv.old;
 	       env = env';
-	       modinfo = senv.modinfo;
+	       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 }
+       | SFBalias (mp',cst) ->
+	   let env' = Option.fold_right 
+	     Environ.add_constraints cst senv.env in
+	   let mp = MPdot(senv.modinfo.modpath, l) in
+	   let env' = register_alias mp mp' env' in
+	     { old = senv.old;
+	       env = env';
+	       modinfo = senv.modinfo;
+	       labset = Labset.add l senv.labset;
+	       revstruct = (l,SFBalias (mp,cst))::senv.revstruct;
                univ = senv.univ;
                engagement = senv.engagement;
 	       imports = senv.imports;
 	       loads = senv.loads;
-               local_retroknowledge = senv.local_retroknowledge }       
+               local_retroknowledge = senv.local_retroknowledge }
        | SFBmodtype mtb ->
 	   let env' = add_modtype_constraints senv.env mtb in
 	   let mp = MPdot(senv.modinfo.modpath, l) in
-	   let env'' = Environ.add_modtype mp (mtb,None) env' in
+	   let env'' = Environ.add_modtype mp mtb env' in
 	     { old = senv.old;
 	       env = env'';
 	       modinfo = senv.modinfo;
@@ -459,7 +529,10 @@ let end_module l restype senv =
 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 = translate_struct_entry senv.env mte in
+  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 env = full_add_module (MPbound mbid) (module_body_of_type mtb) senv.env 
   in
   let new_variant = match senv.modinfo.variant with
@@ -490,7 +563,8 @@ let start_modtype l senv =
 		  modpath = mp;
 		  seed = senv.modinfo.seed;
 		  label = l;
-		  variant = SIG [] }
+		  variant = SIG [];
+		  alias_subst = empty_subst }
   in
   mp, { old = senv;
 	env = senv.env;
@@ -517,7 +591,7 @@ let end_modtype l senv =
   let auto_tb = 
      SEBstruct (modinfo.msid, List.rev senv.revstruct)
   in
-  let mtb = 
+  let mtb_expr = 
     List.fold_left
       (fun mtb (arg_id,arg_b) -> 
 	 SEBfunctor(arg_id,arg_b,mtb))
@@ -536,11 +610,15 @@ let end_modtype l senv =
       newenv
       (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 newenv = 
-    add_modtype_constraints newenv mtb 
+    add_modtype_constraints newenv mtb
   in
   let newenv = 
-    Environ.add_modtype mp (mtb,None) newenv
+    Environ.add_modtype mp mtb newenv
   in 
   mp, { old = oldsenv.old;
 	env = newenv;
@@ -607,7 +685,8 @@ let start_library dir senv =
 		  modpath = mp;
 		  seed = dir;
 		  label = l;
-		  variant = LIBRARY dir }
+		  variant = LIBRARY dir;
+		  alias_subst = empty_subst }
   in
   mp, { old = senv;
 	env = senv.env;
@@ -637,8 +716,8 @@ let export senv dir =
   let mb = 
     { mod_expr = Some (SEBstruct (modinfo.msid, List.rev senv.revstruct));
       mod_type = None;
-      mod_equiv = None;
       mod_constraints = senv.univ;
+      mod_alias = senv.modinfo.alias_subst;
       mod_retroknowledge = senv.local_retroknowledge}
   in
     modinfo.msid, (dir,mb,senv.imports,engagement senv.env)
@@ -692,15 +771,20 @@ let import (dp,mb,depends,engmt) digest senv =
 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 _) as x -> x
+    | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x
     | SFBmodule m -> SFBmodule (lighten_module m)
-    | SFBmodtype m -> SFBmodtype (lighten_modexpr m))
+    | SFBmodtype m -> SFBmodtype 
+	({m with 
+	    typ_expr = lighten_modexpr m.typ_expr}))
   in
     List.map lighten_body struc
 
 and lighten_modexpr = function
   | SEBfunctor (mbid,mty,mexpr) ->
-      SEBfunctor (mbid,lighten_modexpr mty,lighten_modexpr mexpr)
+      SEBfunctor (mbid, 
+		    ({mty with 
+			typ_expr = lighten_modexpr mty.typ_expr}),
+		  lighten_modexpr mexpr)
   | SEBident mp as x -> x
   | SEBstruct (msid, struc) ->
       SEBstruct (msid, lighten_struct struc)
@@ -708,7 +792,7 @@ and lighten_modexpr = function
       SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
   | SEBwith (seb,wdcl) ->
       SEBwith (lighten_modexpr seb,wdcl) 
-
+ 
 let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s)
 
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e764312b52..07f82876f6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -57,6 +57,10 @@ val add_module :
   label -> module_entry -> safe_environment 
     -> module_path * safe_environment
 
+(* Adding a module alias*)
+val add_alias :
+  label -> module_path -> safe_environment 
+    -> module_path * safe_environment
 (* Adding a module type *)
 val add_modtype :
   label -> module_struct_entry -> safe_environment 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 3db187a0b0..e4b1f7045c 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -32,7 +32,8 @@ type namedobject =
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
   | Module of module_body
-  | Modtype of struct_expr_body
+  | Modtype of module_type_body
+  | Alias of module_path
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
@@ -63,6 +64,7 @@ let make_label_map mp list =
        add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
     | SFBmodule mb -> add_map (Module mb)
     | SFBmodtype mtb -> add_map (Modtype mtb)
+    | SFBalias (mp,cst) -> add_map (Alias mp)
   in
     List.fold_right add_one list Labmap.empty
 
@@ -289,43 +291,59 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
 	      
 let rec check_modules cst env msid1 l msb1 msb2 =
   let mp = (MPdot(MPself msid1,l)) in
-  let mty1 = strengthen env (type_of_mb env msb1) mp in
-  let cst = check_modtypes cst env mty1 (type_of_mb env msb2) false in
-    begin
-    match msb1.mod_equiv, msb2.mod_equiv with
-      | _, None -> ()
-      | None, Some mp2 -> 
-	  check_modpath_equiv env mp mp2
-      | Some mp1, Some mp2 ->
-	  check_modpath_equiv env mp1 mp2
-  end;
-  cst
+  let mty1 = module_type_of_module (Some mp) msb1 in
+  let mty2 =  module_type_of_module None msb2 in
+  let cst = check_modtypes cst env mty1 mty2 false in
+    cst
 	
 
-and check_signatures cst env (msid1,sig1) (msid2,sig2') = 
+and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = 
   let mp1 = MPself msid1 in
   let env = add_signature mp1 sig1 env in 
-  let sig2 = subst_signature_msid msid2 mp1 sig2' in
+  let alias = update_subst_alias alias (map_msid msid2 mp1) in
+  let sig2 = subst_structure alias sig2' in
+  let sig2 = subst_signature_msid msid2 mp1 sig2 in
   let map1 = make_label_map mp1 sig1 in
   let check_one_body cst (l,spec2) = 
     let info1 = 
       try 
 	Labmap.find l map1 
       with 
-	  Not_found -> error_no_such_label_sub l (string_of_msid msid1) (string_of_msid msid2)
+	  Not_found -> error_no_such_label_sub l 
+	    (string_of_msid msid1) (string_of_msid msid2)
     in
       match spec2 with
 	| SFBconst cb2 ->
 	    check_constant cst env msid1 l info1 cb2 spec2
 	| SFBmind mib2 -> 
 	    check_inductive cst env msid1 l info1 mib2 spec2
-	| SFBmodule msb2 -> 
-	    let msb1 = 
+	| SFBmodule msb2 ->  
+	    begin
 	      match info1 with
-		| Module msb -> msb
+		| Module msb -> check_modules cst env msid1 l msb msb2
+		| Alias mp ->let msb = 
+		    {mod_expr = Some (SEBident mp);
+		     mod_type = Some (eval_struct env (SEBident mp));
+		     mod_constraints = Constraint.empty;
+		     mod_alias = (lookup_modtype mp env).typ_alias;
+		     mod_retroknowledge = []} in
+		    check_modules cst env msid1 l msb msb2
 		| _ -> error_not_match l spec2
-	    in
-	      check_modules cst env msid1 l msb1 msb2
+	    end
+	| SFBalias (mp,_) ->
+	    begin	
+	      match info1 with
+		| Alias mp1 -> check_modpath_equiv env mp mp1; cst
+		| Module msb -> 
+		    let msb1 = 
+		      {mod_expr = Some (SEBident mp);
+		       mod_type = Some (eval_struct env (SEBident mp));
+		       mod_constraints = Constraint.empty;
+		       mod_alias = (lookup_modtype mp env).typ_alias;
+		       mod_retroknowledge = []} in
+			check_modules cst env msid1 l msb msb1
+		| _ -> error_not_match l spec2
+	    end
 	| SFBmodtype mtb2 ->
 	    let mtb1 = 
 	      match info1 with
@@ -336,35 +354,46 @@ and check_signatures cst env (msid1,sig1) (msid2,sig2') =
   in
     List.fold_left check_one_body cst sig2
     
+
 and check_modtypes cst env mtb1 mtb2 equiv = 
   if mtb1==mtb2 then cst else (* just in case  :) *)
-  let mtb1' = eval_struct env mtb1 in
-  let mtb2' = eval_struct env mtb2 in
-    if mtb1'==mtb2' then cst else
-    match mtb1', mtb2' with
-      | SEBstruct (msid1,list1), 
-	SEBstruct (msid2,list2) -> 
-	  let cst = check_signatures cst env (msid1,list1) (msid2,list2) in
-	  if equiv then
-	    check_signatures cst env (msid2,list2) (msid1,list1) 
-	  else
-	    cst
-      | SEBfunctor (arg_id1,arg_t1,body_t1), 
-	SEBfunctor (arg_id2,arg_t2,body_t2) ->
-	  let cst = check_modtypes cst env arg_t2 arg_t1 equiv in 
-	    (* contravariant *)
-	  let env = 
-	    add_module (MPbound arg_id2) (module_body_of_type arg_t2) env 
-	  in
-	  let body_t1' = 
-            (* since we are just checking well-typedness we do not need
-               to expand any constant. Hence the identity resolver. *)
-	    subst_modtype 
-              (map_mbid arg_id1 (MPbound arg_id2) None)
-	      body_t1
-	  in
-	  check_modtypes cst env body_t1' body_t2 equiv
-      | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+  let mtb1',mtb2'=
+    (match mtb1.typ_strength with
+	 None -> eval_struct env mtb1.typ_expr,
+	   eval_struct env mtb2.typ_expr
+       | Some mp -> strengthen  env mtb1.typ_expr mp,
+	   eval_struct env mtb2.typ_expr) in
+      let rec check_structure cst env str1 str2 equiv = 
+	match str1, str2 with
+	  | SEBstruct (msid1,list1), 
+	    SEBstruct (msid2,list2) -> 
+	      let cst = check_signatures cst env
+		(msid1,list1) mtb1.typ_alias (msid2,list2) in
+		if equiv then
+		  check_signatures cst env 
+		    (msid2,list2) mtb2.typ_alias  (msid1,list1) 
+		else
+		  cst
+	  | SEBfunctor (arg_id1,arg_t1,body_t1), 
+	      SEBfunctor (arg_id2,arg_t2,body_t2) ->
+	      let cst = check_modtypes cst env arg_t2 arg_t1 equiv in 
+		(* contravariant *)
+	      let env = 
+		add_module (MPbound arg_id2) (module_body_of_type arg_t2) env 
+	      in
+	      let body_t1' = 
+		(* since we are just checking well-typedness we do not need
+		   to expand any constant. Hence the identity resolver. *)
+		subst_struct_expr
+		  (map_mbid arg_id1 (MPbound arg_id2) None)
+		  body_t1
+	      in
+		check_structure cst env (eval_struct env body_t1')
+		  (eval_struct env body_t2) equiv
+	  | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+      in 
+     if mtb1'== mtb2' then cst 
+     else check_structure cst env mtb1' mtb2' equiv
 	  
 let check_subtypes env sup super = 
   check_modtypes Constraint.empty env sup super false
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index d7288fc065..c0b1ee5d3c 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -14,6 +14,6 @@ open Declarations
 open Environ
 (*i*)
 
-val check_subtypes : env -> struct_expr_body -> struct_expr_body -> constraints
+val check_subtypes : env -> module_type_body -> module_type_body -> constraints