Beaoucoup de changements dans la representation interne des modules.

kernel:

-declaration.ml
   unification des representations pour les modules et modules types.
     (type struct_expr_body)

-mod_typing.ml
   le typage des modules est separe de l'evaluation des modules

-modops.ml
   nouvelle fonction qui pour toutes expressions de structure calcule
   sa forme evaluee.(eval_struct)

-safe_typing.ml
  ajout du support du nouvel operateur Include.(add_include).


library:

-declaremods.ml
   nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
   les alias via la nametab.

parsing:

-g_vernac.ml4:
   nouvelles regles pour le support des Includes et pour l'application des signatures
   fonctorielles.


extraction:
  Adaptation a la nouvelle representation des modules et support de l'operateur with.




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

16 files changed, 657 insertions, 571 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 4a5893de8..63c690d48 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -247,44 +247,31 @@ let subst_mind sub mib =
 (*s Modules: signature component specifications, module types, and
   module declarations *)
 
-type specification_body = 
-  | SPBconst of constant_body
-  | SPBmind of mutual_inductive_body
-  | SPBmodule of module_specification_body
-  | SPBmodtype of module_type_body
-
-and module_signature_body = (label * specification_body) list
-
-and module_type_body = 
-  | MTBident of kernel_name
-  | MTBfunsig of mod_bound_id * module_type_body * module_type_body
-  | MTBsig of mod_self_id * module_signature_body
-
-and module_specification_body = 
-    { msb_modtype : module_type_body;
-      msb_equiv : module_path option; 
-      msb_constraints : constraints }
-
-type structure_elem_body = 
-  | SEBconst of constant_body
-  | SEBmind of mutual_inductive_body
-  | SEBmodule of module_body
-  | SEBmodtype of module_type_body
-
-and module_structure_body = (label * structure_elem_body) list
-
-and module_expr_body =
-  | MEBident of module_path
-  | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
-  | MEBstruct of mod_self_id * module_structure_body
-  | MEBapply of module_expr_body * module_expr_body
+type structure_field_body = 
+  | SFBconst of constant_body
+  | SFBmind of mutual_inductive_body
+  | SFBmodule of module_body
+  | SFBmodtype of struct_expr_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 
+  | SEBstruct of mod_self_id * structure_body
+  | SEBapply of struct_expr_body * struct_expr_body
       * constraints
+  | SEBwith of struct_expr_body * with_declaration_body
 
+and with_declaration_body =
+    With_module_body of identifier list * module_path * constraints
+  | With_definition_body of  identifier list * constant_body
+        
 and module_body = 
-    { mod_expr : module_expr_body option;
-      mod_user_type : module_type_body option;
-      mod_type : module_type_body;
+    { mod_expr : struct_expr_body option;
+      mod_type : struct_expr_body option;
       mod_equiv : module_path option;
       mod_constraints : constraints;
       mod_retroknowledge : Retroknowledge.action list}
 
+type module_type_body = struct_expr_body * module_path option
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2f32d8639..544cea246 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -177,51 +177,32 @@ val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
 (*s Modules: signature component specifications, module types, and
   module declarations *)
 
-type specification_body = 
-  | SPBconst of constant_body
-  | SPBmind of mutual_inductive_body
-  | SPBmodule of module_specification_body
-  | SPBmodtype of module_type_body
-
-and module_signature_body = (label * specification_body) list
-
-and module_type_body = 
-  | MTBident of kernel_name
-  | MTBfunsig of mod_bound_id * module_type_body * module_type_body
-  | MTBsig of mod_self_id * module_signature_body
-
-and module_specification_body = 
-    { msb_modtype : module_type_body;
-      msb_equiv : module_path option; 
-      msb_constraints : constraints }
-    (*    [type_of](equiv) <: modtype  (if given)  
-       +  substyping of past [With_Module] mergers *)
-
-
-type structure_elem_body = 
-  | SEBconst of constant_body
-  | SEBmind of mutual_inductive_body
-  | SEBmodule of module_body
-  | SEBmodtype of module_type_body
-
-and module_structure_body = (label * structure_elem_body) list
-
-and module_expr_body =
-  | MEBident of module_path
-  | MEBfunctor of mod_bound_id * module_type_body * module_expr_body 
-  | MEBstruct of mod_self_id * module_structure_body
-  | MEBapply of module_expr_body * module_expr_body  (* (F A) *)
-      * constraints  (* [type_of](A) <: [input_type_of](F) *)
+type structure_field_body = 
+  | SFBconst of constant_body
+  | SFBmind of mutual_inductive_body
+  | SFBmodule of module_body
+  | SFBmodtype of struct_expr_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 
+  | SEBstruct of mod_self_id * structure_body
+  | SEBapply of struct_expr_body * struct_expr_body
+      * constraints
+  | SEBwith of struct_expr_body * with_declaration_body
+
+and with_declaration_body =
+    With_module_body of identifier list * module_path * constraints
+  | With_definition_body of identifier list * constant_body
 
 and module_body = 
-    { mod_expr : module_expr_body option;
-      mod_user_type : module_type_body option;
-      mod_type : module_type_body;
+    { mod_expr : struct_expr_body option;
+      mod_type : struct_expr_body option;
       mod_equiv : module_path option;
       mod_constraints : constraints;
       mod_retroknowledge : Retroknowledge.action list}
-    (*    [type_of(mod_expr)]  <: [mod_user_type] (if given)  *)
-    (*  if equiv given then constraints are empty *)
-
 
 
+type module_type_body = struct_expr_body * module_path option
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 17da967c2..89e444a74 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -74,28 +74,22 @@ type specification_entry =
     SPEconst of constant_entry
   | SPEmind of mutual_inductive_entry
   | SPEmodule of module_entry
-  | SPEmodtype of module_type_entry
+  | SPEmodtype of module_struct_entry
 
-and module_type_entry = 
-    MTEident of kernel_name
-  | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
-  | MTEwith of module_type_entry * with_declaration
-
-and module_signature_entry = (label * specification_entry) list
+and module_struct_entry = 
+    MSEident of module_path
+  | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
+  | MSEwith of module_struct_entry * with_declaration
+  | MSEapply of module_struct_entry * module_struct_entry
 
 and with_declaration = 
     With_Module of identifier list * module_path
   | With_Definition of identifier list * constr
 
-and module_expr = 
-    MEident of module_path
-  | MEfunctor of mod_bound_id * module_type_entry * module_expr
-  | MEapply of module_expr * module_expr
-
 and module_structure = (label * specification_entry) list
 
-
 and module_entry = 
-    { mod_entry_type : module_type_entry option;
-      mod_entry_expr : module_expr option}
+    { mod_entry_type : module_struct_entry option;
+      mod_entry_expr : module_struct_entry option}
+
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 56ea852da..b757032f8 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -73,28 +73,22 @@ type specification_entry =
     SPEconst of constant_entry
   | SPEmind of mutual_inductive_entry
   | SPEmodule of module_entry
-  | SPEmodtype of module_type_entry
+  | SPEmodtype of module_struct_entry
 
-and module_type_entry = 
-    MTEident of kernel_name
-  | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
-  | MTEwith of module_type_entry * with_declaration
-
-and module_signature_entry = (label * specification_entry) list
+and module_struct_entry = 
+    MSEident of module_path
+  | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
+  | MSEwith of module_struct_entry * with_declaration
+  | MSEapply of module_struct_entry * module_struct_entry
 
 and with_declaration = 
     With_Module of identifier list * module_path
   | With_Definition of identifier list * constr
 
-and module_expr = 
-    MEident of module_path
-  | MEfunctor of mod_bound_id * module_type_entry * module_expr
-  | MEapply of module_expr * module_expr
-
 and module_structure = (label * specification_entry) list
 
-
 and module_entry = 
-    { mod_entry_type : module_type_entry option;
-      mod_entry_expr : module_expr option}
+    { mod_entry_type : module_struct_entry option;
+      mod_entry_expr : module_struct_entry option}
+
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index c2ec6ea7e..b1290452a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -160,7 +160,7 @@ let add_constant kn cs env =
 (* constant_type gives the type of a constant *)
 let constant_type env kn =
   let cb = lookup_constant kn env in
-  cb.const_type  
+    cb.const_type  
 
 type const_evaluation_result = NoBody | Opaque
 
@@ -273,7 +273,7 @@ let keep_hyps env needed =
 (* Modules *)
 
 let add_modtype ln mtb env = 
-  let new_modtypes = KNmap.add ln mtb env.env_globals.env_modtypes in
+  let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
   let new_globals = 
     { env.env_globals with 
 	env_modtypes = new_modtypes } in
@@ -290,7 +290,8 @@ let lookup_module mp env =
   MPmap.find mp env.env_globals.env_modules
 
 let lookup_modtype ln env = 
-  KNmap.find ln env.env_globals.env_modtypes
+  MPmap.find ln env.env_globals.env_modtypes
+
 
 (*s Judgments. *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index bfbb5dd3c..10e962674 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -146,13 +146,13 @@ val scrape_mind : env -> mutual_inductive -> mutual_inductive
 
 (************************************************************************)
 (*s Modules *)
-val add_modtype : kernel_name -> module_type_body -> env -> env
+val add_modtype : module_path -> module_type_body -> env -> env
 
 (* [shallow_add_module] does not add module components *)
 val shallow_add_module : module_path -> module_body -> env -> env
 
 val lookup_module : module_path -> env -> module_body
-val lookup_modtype : kernel_name -> env -> module_type_body
+val lookup_modtype : module_path -> env -> module_type_body
 
 (************************************************************************)
 (*s Universe constraints *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 93d01f12a..201835c10 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -22,14 +22,9 @@ open Mod_subst
 exception Not_path
 
 let path_of_mexpr = function
-  | MEident mb -> mb
+  | MSEident mb -> mb
   | _ -> raise Not_path
 
-let rec replace_first p k = function 
-  | [] -> [] 
-  | h::t when p h -> k::t
-  | h::t -> h::(replace_first p k t)
-
 let rec list_split_assoc k rev_before = function
   | [] -> raise Not_found
   | (k',b)::after when k=k' -> rev_before,b,after
@@ -42,25 +37,88 @@ let rec list_fold_map2 f e = function
        let e'',t1',t2' = list_fold_map2 f e' t in
 	 e'',h1'::t1',h2'::t2'
 
-let type_modpath env mp = 
-  strengthen env (lookup_module mp env).mod_type mp
+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))
+    | With_Module (id,mp) -> 
+	let cst = check_with_aux_mod env mtb with_decl in
+	  SEBwith(mtb,With_module_body(id,mp,cst))
 
-let rec translate_modtype env mte =
-  match mte with
-    | MTEident ln -> MTBident ln
-    | MTEfunsig (arg_id,arg_e,body_e) -> 
-	let arg_b = translate_modtype env arg_e in
-	let env' = 
-	  add_module (MPbound arg_id) (module_body_of_type arg_b) env in
-	let body_b = translate_modtype env' body_e in
-	  MTBfunsig (arg_id,arg_b,body_b)
-    | MTEwith (mte, with_decl) ->
-	let mtb = translate_modtype env mte in
-	  merge_with env mtb with_decl
+and check_with_aux_def env mtb with_decl = 
+  let msid,sig_b = match (eval_struct env mtb) with 
+    | SEBstruct(msid,sig_b) ->
+	msid,sig_b
+    | _ -> error_signature_expected mtb
+  in
+  let id,idl = match with_decl with 
+    | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
+    | With_Definition ([],_) | With_Module ([],_) -> assert false
+  in
+  let l = label_of_id id in
+    try
+      let rev_before,spec,after = list_split_assoc l [] sig_b in
+      let before = List.rev rev_before in
+      let env' = Modops.add_signature (MPself msid) before env in
+	match with_decl with
+          | With_Definition ([],_) -> assert false
+	  | With_Definition ([id],c) -> 
+	      let cb = match spec with
+		  SFBconst cb -> cb
+		| _ -> error_not_a_constant l
+	      in 
+		begin
+		  match cb.const_body with
+		    | None -> 
+			let (j,cst1) = Typeops.infer env' c in
+			let typ = Typeops.type_of_constant_type env' cb.const_type in
+			let cst2 = Reduction.conv_leq env' j.uj_type typ in
+			let cst = 
+			  Constraint.union 
+			    (Constraint.union cb.const_constraints cst1)
+			    cst2 in
+			let body = Some (Declarations.from_val j.uj_val) in
+			let cb' = {cb with 
+				     const_body = body;
+				     const_body_code = Cemitcodes.from_val
+                            (compile_constant_body env' body false false);
+                                     const_constraints = cst} in
+			  cb'
+		    | Some b -> 
+			let cst1 = Reduction.conv env' c (Declarations.force b) in
+			let cst = Constraint.union cb.const_constraints cst1 in
+			let body = Some (Declarations.from_val c) in
+			let cb' = {cb with 
+				     const_body = body;
+				     const_body_code = Cemitcodes.from_val
+                            (compile_constant_body env' body false false);
+                                     const_constraints = cst} in
+			  cb'
+	      end
+	  | With_Definition (_::_,_) ->
+	      let old = match spec with
+		  SFBmodule msb -> msb
+		| _ -> error_not_a_module (string_of_label l)
+	      in
+		begin
+		  match old.mod_equiv 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 ->
+			error_a_generative_module_expected l
+		end
+	  | _ -> anomaly "Modtyping:incorrect use of with"
+    with
+	Not_found -> error_no_such_label l
+      | Reduction.NotConvertible -> error_with_incorrect l
 
-and merge_with env mtb with_decl = 
-  let msid,sig_b = match (Modops.scrape_modtype env mtb) with 
-    | MTBsig(msid,sig_b) -> let msid'=(refresh_msid msid) in
+and check_with_aux_mod env mtb with_decl = 
+  let 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)
     | _ -> error_signature_expected mtb
   in
@@ -73,107 +131,58 @@ and merge_with env mtb with_decl =
       let rev_before,spec,after = list_split_assoc l [] sig_b in
       let before = List.rev rev_before in
       let env' = Modops.add_signature (MPself msid) before env in
-      let new_spec = match with_decl with
-        | With_Definition ([],_)
-        | With_Module ([],_) -> assert false
-	| With_Definition ([id],c) -> 
-	    let cb = match spec with
-		SPBconst cb -> cb
-	      | _ -> error_not_a_constant l
-	    in 
-	      begin
-		match cb.const_body with
-		  | None -> 
-		      let (j,cst1) = Typeops.infer env' c in
-		      let typ = Typeops.type_of_constant_type env' cb.const_type in
-		      let cst2 = Reduction.conv_leq env' j.uj_type typ in
-		      let cst = 
-			Constraint.union 
-			  (Constraint.union cb.const_constraints cst1)
-			  cst2 in
-                      let body = Some (Declarations.from_val j.uj_val) in
-			SPBconst {cb with 
-				    const_body = body;
-			            const_body_code = Cemitcodes.from_val
-                        (compile_constant_body env' body false false);
-                                    const_constraints = cst}
-		  | Some b -> 
-		      let cst1 = Reduction.conv env' c (Declarations.force b) in
-		      let cst = Constraint.union cb.const_constraints cst1 in
-                      let body = Some (Declarations.from_val c) in
-			SPBconst {cb with 
-				    const_body = body;
-				    const_body_code = Cemitcodes.from_val
-                        (compile_constant_body env' body false false);
-                                    const_constraints = cst}
-	      end	
-(* and what about msid's ????? Don't they clash ? *)
-	| With_Module ([id], mp) ->
-	    let old = match spec with
-		SPBmodule msb -> msb
-	      | _ -> error_not_a_module (string_of_label l)
-	    in
-	    let mtb = type_modpath env' mp in
-	    let cst =
-              try check_subtypes env' mtb old.msb_modtype
+	match with_decl with
+          | With_Module ([],_) -> assert false
+	  | With_Module ([id], mp) ->
+	      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 cst =
+		try check_subtypes env' mtb' (type_of_mb env old)
               with Failure _ -> error_with_incorrect (label_of_id id) in
-	    let equiv = 
- 	      match old.msb_equiv with
+	      let _ = 
+ 		match old.mod_equiv with
 		| None -> Some mp
 		| Some mp' -> 
 		    check_modpath_equiv env' mp mp';
 		    Some mp
-	    in
-	    let msb =
-	      {msb_modtype = mtb; 
-	       msb_equiv = equiv; 
-	       msb_constraints = Constraint.union old.msb_constraints cst }
-	    in
-	      SPBmodule msb
-	| With_Definition (_::_,_)
+	      in
+		cst
         | With_Module (_::_,_) -> 
 	    let old = match spec with
-		SPBmodule msb -> msb
+		SFBmodule msb -> msb
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
 	      begin
-		match old.msb_equiv 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
-                    let modtype = 
-                     merge_with env' old.msb_modtype new_with_decl in
-                    let msb =
-	              {msb_modtype = modtype; 
-	               msb_equiv = None; 
-	               msb_constraints = old.msb_constraints }
-	            in
-	             SPBmodule msb
-                 | Some mp ->
-                    error_a_generative_module_expected l
+		match old.mod_equiv 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_mod env' (type_of_mb env old) new_with_decl 
+                  | Some mp ->
+                      error_a_generative_module_expected l
               end
-      in
-	MTBsig(msid,  before@(l,new_spec)::after)
+	| _ -> anomaly "Modtyping:incorrect use of with"
     with
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
-
-
-and translate_module env  me =
+	  
+and translate_module env me =
   match me.mod_entry_expr, me.mod_entry_type with
     | None, None -> 
 	anomaly "Mod_typing.translate_module: empty type and expr in module entry"
     | None, Some mte -> 
-	let mtb = translate_modtype env mte in
+	let mtb = translate_struct_entry env mte in
 	{ mod_expr = None;
-	  mod_user_type = Some mtb;
-	  mod_type = mtb;
+	  mod_type = Some mtb;
 	  mod_equiv = None;
-	  mod_constraints = Constraint.empty;
-	  mod_retroknowledge = [] } 
+	  mod_constraints = Constraint.empty; 
+	  mod_retroknowledge = []}
     | Some mexpr, _ -> 
-	let meq_o = (* do we have a transparent module ? *)
+	let meq_o = 
 	  try       (* TODO: transparent field in module_entry *)
 	    match me.mod_entry_type with
 	      | None -> Some (path_of_mexpr mexpr)
@@ -181,17 +190,17 @@ and translate_module env  me =
 	  with 
 	    | Not_path -> None
 	in
-	let meb,mtb1 = translate_mexpr env mexpr in
-	let mtb, mod_user_type, cst =
+	let meb = translate_struct_entry env mexpr in
+	let mod_typ, cst =
 	  match me.mod_entry_type with
-	    | None -> mtb1, None, Constraint.empty
+	    | None ->  None, Constraint.empty
 	    | Some mte -> 
-		let mtb2 = translate_modtype env mte in
-                let cst = check_subtypes env mtb1 mtb2 in
-		mtb2, Some mtb2, cst
+		let mtb1 = translate_struct_entry env mte in
+                let cst = check_subtypes env (eval_struct env meb)
+		  mtb1 in
+		  Some mtb1, cst
 	in
-	  { mod_type = mtb;
-	    mod_user_type = mod_user_type;
+	  { mod_type = mod_typ;
 	    mod_expr = Some meb;
 	    mod_equiv = meq_o;
 	    mod_constraints = cst;
@@ -200,96 +209,78 @@ and translate_module env  me =
 					If it does, I don't really know how to
 					fix the bug.*)
 
-(* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *)
-and translate_mexpr env mexpr = match mexpr with
-  | MEident mp -> 
-      MEBident mp,
-      type_modpath env mp
-  | MEfunctor (arg_id, arg_e, body_expr) ->
-      let arg_b = translate_modtype env arg_e in
+
+and translate_struct_entry env mse = match mse with
+  | MSEident mp -> 
+      SEBident mp
+  | 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,body_tb) = translate_mexpr env' body_expr in
-	MEBfunctor (arg_id, arg_b, body_b), 
-	MTBfunsig (arg_id, arg_b, body_tb)
-  | MEapply (fexpr,mexpr) ->
-      let feb,ftb = translate_mexpr env fexpr in
-      let ftb = scrape_modtype env ftb in
-      let farg_id, farg_b, fbody_b = destr_functor ftb in
-      let meb,mtb = translate_mexpr env mexpr in
-      let cst = check_subtypes env mtb farg_b in
-      let mp = 
+      let body_b = translate_struct_entry env' body_expr in
+	SEBfunctor (arg_id, arg_b, body_b)
+  | MSEapply (fexpr,mexpr) ->
+      let feb = 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 _ = 
 	try
 	  path_of_mexpr mexpr 
 	with
 	  | Not_path -> error_application_to_not_path mexpr
-	      (* place for nondep_supertype *)
-      in
-       let resolve = Modops.resolver_of_environment farg_id farg_b mp env in
-	MEBapply(feb,meb,cst),
-        (* This is the place where the functor formal parameter is
-           substituted by the given argument to compute the type of the
-           functor application. *)
-	subst_modtype 
-         (map_mbid farg_id mp (Some resolve)) fbody_b
- 
+	      (* 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)
+  | MSEwith(mte, with_decl) ->
+	let mtb = translate_struct_entry env mte in
+	let mtb' = check_with env mtb with_decl in
+	  mtb'
 
-let translate_module env me = translate_module env  me
 
-let rec add_module_expr_constraints env = function
-  | MEBident _ -> env
+let rec add_struct_expr_constraints env = function
+  | SEBident _ -> env
 
-  | MEBfunctor (_,mtb,meb) -> 
-      add_module_expr_constraints (add_modtype_constraints env mtb) meb
+  | SEBfunctor (_,mtb,meb) -> 
+      add_struct_expr_constraints 
+	(add_modtype_constraints env mtb) meb
 
-  | MEBstruct (_,mod_struct_body) ->
+  | SEBstruct (_,structure_body) ->
       List.fold_left 
         (fun env (l,item) -> add_struct_elem_constraints env item)
         env
-        mod_struct_body
+        structure_body
 
-  | MEBapply (meb1,meb2,cst) ->
+  | SEBapply (meb1,meb2,cst) ->
       Environ.add_constraints cst 
-        (add_module_expr_constraints 
-	  (add_module_expr_constraints env meb1) 
+        (add_struct_expr_constraints 
+	  (add_struct_expr_constraints env meb1) 
 	  meb2)
-
+  | SEBwith(meb,With_definition_body(_,cb))->
+      Environ.add_constraints cb.const_constraints
+	(add_struct_expr_constraints env meb)
+  | SEBwith(meb,With_module_body(_,_,cst))->
+      Environ.add_constraints cst
+	(add_struct_expr_constraints env meb)	
+		
 and add_struct_elem_constraints env = function 
-  | SEBconst cb -> Environ.add_constraints cb.const_constraints env
-  | SEBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SEBmodule mb -> add_module_constraints env mb
-  | SEBmodtype mtb -> add_modtype_constraints env mtb
+  | 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
+  | SFBmodtype mtb -> add_modtype_constraints env mtb
 
 and add_module_constraints env mb = 
-  (* if there is a body, the mb.mod_type is either inferred from the
-     body and hence uninteresting or equal to the non-empty
-     user_mod_type *)
   let env = match mb.mod_expr with
-    | None -> add_modtype_constraints env mb.mod_type
-    | Some meb -> add_module_expr_constraints env meb
+    | None -> env
+    | Some meb -> add_struct_expr_constraints env meb
   in
-  let env = match mb.mod_user_type with
+  let env = match mb.mod_type with
     | None -> env
-    | Some mtb -> add_modtype_constraints env mtb
+    | Some mtb -> 
+	add_modtype_constraints env mtb
   in
     Environ.add_constraints mb.mod_constraints env
 
-and add_modtype_constraints env = function
-  | MTBident _ -> env
-  | MTBfunsig (_,mtb1,mtb2) ->
-      add_modtype_constraints
-        (add_modtype_constraints env mtb1)
-        mtb2
-  | MTBsig (_,mod_sig_body) ->
-      List.fold_left 
-        (fun env (l,item) -> add_sig_elem_constraints env item)
-        env
-        mod_sig_body
-
-and add_sig_elem_constraints env = function 
-  | SPBconst cb -> Environ.add_constraints cb.const_constraints env
-  | SPBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SPBmodule {msb_modtype=mtb; msb_constraints=cst} -> 
-      add_modtype_constraints (Environ.add_constraints cst env) mtb
-  | SPBmodtype mtb -> add_modtype_constraints env mtb
-
-
+and add_modtype_constraints env mtb = 
+  add_struct_expr_constraints env mtb
+      
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 702e79ecc..124cb89c4 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -15,13 +15,13 @@ open Entries
 (*i*)
 
 
-val translate_modtype : env -> module_type_entry -> module_type_body
-
 val translate_module : env -> module_entry -> module_body
 
-val translate_mexpr : env -> module_expr -> module_expr_body * module_type_body
+val translate_struct_entry : env -> module_struct_entry -> struct_expr_body
 
-val add_modtype_constraints : env -> module_type_body -> env
+val add_modtype_constraints : env -> struct_expr_body -> env
 
 val add_module_constraints : env -> module_body -> env
 
+
+
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 135a37747..c5b8e15b5 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -83,43 +83,36 @@ let error_local_context lo =
 
 
 let error_no_such_label_sub l l1 l2 =
-  error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing (or invisible) in "^l1^".")
+  error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing in "^l1^".")
 
-let rec scrape_modtype env = function
-  | MTBident kn -> scrape_modtype env (lookup_modtype kn env)
-  | mtb -> mtb
+
+
+let rec list_split_assoc k rev_before = function
+  | [] -> raise Not_found
+  | (k',b)::after when k=k' -> rev_before,b,after
+  | h::tail -> list_split_assoc k (h::rev_before) tail
+
+let path_of_seb = function
+  | SEBident mb -> mb
+  | _ -> anomaly "Modops: evaluation failed."
+
+
+let destr_functor env mtb =
+  match mtb with
+  | SEBfunctor (arg_id,arg_t,body_t) ->
+      	    (arg_id,arg_t,body_t)
+  | _ -> error_not_a_functor mtb
 
 (* the constraints are not important here *)
-let module_body_of_spec msb = 
-    { mod_type = msb.msb_modtype;
-      mod_equiv = msb.msb_equiv;
-      mod_expr = None;
-      mod_user_type = None;
-      mod_constraints = Constraint.empty;
-      mod_retroknowledge = []}
 
 let module_body_of_type mtb = 
-  { mod_type = mtb;
+  { mod_type = Some mtb;
     mod_equiv = None;
     mod_expr = None;
-    mod_user_type = None;
     mod_constraints = Constraint.empty;
     mod_retroknowledge = []}
 
 
-(* the constraints are not important here *)
-let module_spec_of_body mb = 
-  { msb_modtype = mb.mod_type; 
-    msb_equiv = mb.mod_equiv; 
-    msb_constraints = Constraint.empty}
-
-
-
-let destr_functor = function
-  | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
-  | mtb -> error_not_a_functor mtb
- 
-
 let rec check_modpath_equiv env mp1 mp2 = 
   if mp1=mp2 then () else
   let mb1 = lookup_module mp1 env in
@@ -131,47 +124,62 @@ let rec check_modpath_equiv env mp1 mp2 =
 	      | Some mp2' -> check_modpath_equiv env mp2' mp1)
       | Some mp1' -> check_modpath_equiv env mp2 mp1'
 
+let subst_with_body sub = function
+  | With_module_body(id,mp,cst) ->
+      With_module_body(id,subst_mp sub mp,cst)
+  | With_definition_body(id,cb) ->
+      With_definition_body( id,subst_const_body sub cb)
 
-let rec subst_modtype sub = function
-    (* This is the case in which I am substituting a whole module.
-       For instance "Module M(X). Module N := X. End M". When I apply
-       M to M' I must substitute M' for X in "Module N := X". *)
-  | MTBident ln -> MTBident (subst_kn sub ln)
-  | MTBfunsig (arg_id, arg_b, body_b) ->
-      MTBfunsig (arg_id, 
-		 subst_modtype  sub arg_b, 
-		 subst_modtype  sub body_b)
-  | MTBsig (sid1, msb) -> 
-      MTBsig (sid1, subst_signature sub msb)
-
-and subst_signature sub sign = 
+let rec subst_modtype sub mtb =
+  subst_struct_expr sub mtb
+  
+and subst_structure sub sign = 
   let subst_body  = function
-      SPBconst cb -> 
-	SPBconst (subst_const_body sub cb)
-    | SPBmind mib -> 
-	SPBmind (subst_mind sub mib)
-    | SPBmodule mb -> 
-	SPBmodule (subst_module sub mb)
-    | SPBmodtype mtb -> 
-	SPBmodtype (subst_modtype sub mtb)
+      SFBconst cb -> 
+	SFBconst (subst_const_body sub cb)
+    | SFBmind mib -> 
+	SFBmind (subst_mind sub mib)
+    | SFBmodule mb -> 
+	SFBmodule (subst_module sub mb)
+    | SFBmodtype mtb -> 
+	SFBmodtype (subst_modtype sub mtb)
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
 and subst_module  sub mb =
-  let mtb' = subst_modtype sub mb.msb_modtype in
+  let mtb' = Option.smartmap (subst_modtype 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 mpo' = Option.smartmap (subst_mp sub) mb.msb_equiv in
-    if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else
-      { msb_modtype=mtb'; 
-	msb_equiv=mpo'; 
-	msb_constraints=mb.msb_constraints}
+  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' 
+    then mb else
+      { mod_expr = me';
+	mod_type=mtb'; 
+	mod_equiv=mpo'; 
+	mod_constraints=mb.mod_constraints;
+	mod_retroknowledge=mb.mod_retroknowledge}
+
+
+and subst_struct_expr sub = function
+    | SEBident mp -> SEBident (subst_mp sub  mp)
+    | SEBfunctor (msid, mtb, meb') -> 
+	SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb')
+    | SEBstruct (msid,str)->
+	SEBstruct(msid, subst_structure sub str)
+    | SEBapply (meb1,meb2,cst)->
+	SEBapply(subst_struct_expr sub meb1,
+		 subst_struct_expr sub meb2,
+		 cst)
+    | SEBwith (meb,wdb)-> 
+	SEBwith(subst_struct_expr sub meb,
+		subst_with_body sub wdb)
+ 
 
 let subst_signature_msid msid mp = 
-  subst_signature (map_msid msid mp)
-
+  subst_structure (map_msid msid mp)
 
 (* spiwack: here comes the function which takes care of importing 
    the retroknowledge declared in the library *)
@@ -198,43 +206,150 @@ let add_retroknowledge msid mp =
      imports 10 000 retroknowledge registration.*)
   List.fold_right subst_and_perform lclrk env
 
-(* we assume that the substitution of "mp" into "msid" is already done
-(or unnecessary) *)
-let rec add_signature mp sign env = 
+
+
+let strengthen_const env mp l cb = 
+  match cb.const_opaque, cb.const_body with
+  | false, Some _ -> cb
+  | true, Some _ 
+  | _, None -> 
+      let const = mkConst (make_con mp empty_dirpath l) in 
+      let const_subs = Some (Declarations.from_val const) in
+	{cb with 
+      	   const_body = const_subs;
+	   const_opaque = false;
+           const_body_code = Cemitcodes.from_val
+             (compile_constant_body env const_subs false false)
+	}
+
+let strengthen_mind env mp l mib = match mib.mind_equiv with
+  | Some _ -> mib
+  | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
+
+
+let rec eval_struct env = function 
+  | SEBident mp -> 
+      begin
+	match (lookup_modtype mp env) with
+	    mtb,None -> eval_struct env mtb
+	  | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb)
+      end
+  | SEBapply (seb1,seb2,_) -> 
+      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
+  | mtb -> mtb
+      
+and type_of_mb env mb =
+  match mb.mod_type,mb.mod_expr with
+      None,Some b -> eval_struct env b
+    | Some t, _ -> eval_struct env t
+    | _,_ -> anomaly 
+	"Modops:  empty type and empty expr" 
+	  
+and merge_with env mtb with_decl = 
+  let msid,sig_b = match (eval_struct env mtb) with 
+    | SEBstruct(msid,sig_b) -> msid,sig_b
+    | _ -> error_signature_expected mtb
+  in
+  let id,idl = match with_decl with 
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) -> id,idl
+    | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false
+  in
+  let l = label_of_id id in
+    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
+        | With_definition_body ([],_)
+        | With_module_body ([],_,_) -> assert false
+	| With_definition_body ([id],c) -> 
+	    SFBconst c
+	| 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)
+	| 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 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)
+      in
+	SEBstruct(msid,  before@(l,new_spec)::after)
+    with
+	Not_found -> error_no_such_label l
+
+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
       match elem with
-	| SPBconst cb -> Environ.add_constant con cb env
-	| SPBmind mib -> Environ.add_mind kn mib env
-	| SPBmodule mb -> 
-	    add_module (MPdot (mp,l)) (module_body_of_spec mb) env 
+	| SFBconst cb -> Environ.add_constant con cb env
+	| SFBmind mib -> Environ.add_mind kn mib env
+	| SFBmodule mb -> 
+	    add_module (MPdot (mp,l)) mb env 
 	    (* adds components as well *)
-	| SPBmodtype mtb -> Environ.add_modtype kn mtb env
+	| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) 
+	    (mtb,None) 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
-    match scrape_modtype env mb.mod_type with
-      | MTBident _ -> anomaly "scrape_modtype does not work!"
-      | MTBsig (msid,sign) -> 
+  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 mod_typ = type_of_mb env mb in
+    match mod_typ with
+      | SEBstruct (msid,sign) -> 
 	  add_retroknowledge msid mp (mb.mod_retroknowledge)
 	    (add_signature mp (subst_signature_msid msid mp sign) env)
-      | MTBfunsig _ -> env
+      | SEBfunctor _ -> env
+      | _ -> anomaly "Modops:the evaluation of the structure failed "
+	  
 
 
-let rec constants_of_specification env mp sign =
+and  constants_of_specification env mp sign =
  let aux (env,res) (l,elem) =
   match elem with
-   | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
-   | SPBmind _ -> env,res
-   | SPBmodule mb ->
-       let new_env =  add_module (MPdot (mp,l)) (module_body_of_spec mb) env in 
+   | 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 
        new_env,(constants_of_modtype env (MPdot (mp,l))
-		  (module_body_of_spec mb).mod_type) @ res
-   | SPBmodtype mtb -> 
+		   (type_of_mb env mb)) @ res
+   | SFBmodtype mtb -> 
        (* module type dans un module type. 
 	  Il faut au moins mettre mtb dans l'environnement (avec le bon 
 	  kn pour pouvoir continuer aller deplier les modules utilisant ce 
@@ -250,21 +365,22 @@ let rec 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 (make_kn mp empty_dirpath l) mtb env in 
+       let new_env = Environ.add_modtype (MPdot(mp,l)) (mtb,None) env in 
        new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res
  in
  snd (List.fold_left aux (env,[]) sign)
 
 and constants_of_modtype env mp modtype =
- match scrape_modtype env modtype with
-    MTBident _ -> anomaly "scrape_modtype does not work!"
-  | MTBsig (msid,sign) ->
-     constants_of_specification env mp
-      (subst_signature_msid msid mp sign)
-  | MTBfunsig _ -> []
-
-(* returns a resolver for kn that maps mbid to mp *)
-let resolver_of_environment mbid modtype mp env =
+ 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
  let rec make_resolve = function
    | [] -> []
@@ -284,65 +400,56 @@ let resolver_of_environment mbid modtype mp env =
  let resolve = make_resolve constants in
    Mod_subst.make_resolver resolve
 
-let strengthen_const env mp l cb = 
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _ 
-  | _, None -> 
-      let const = mkConst (make_con mp empty_dirpath l) in 
-      let const_subs = Some (Declarations.from_val const) in
-	{cb with 
-      	   const_body = const_subs;
-	   const_opaque = false;
-           const_body_code = Cemitcodes.from_val
-             (compile_constant_body env const_subs false false)
-	}
-
-let strengthen_mind env mp l mib = match mib.mind_equiv with
-  | Some _ -> mib
-  | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
     
-let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
-  | MTBident _ -> anomaly "scrape_modtype does not work!"
-  | MTBfunsig _ -> mtb
-  | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
-
-and strengthen_mod env mp msb = 
-  { msb_modtype = strengthen_mtb env mp msb.msb_modtype;
-    msb_equiv = begin match msb.msb_equiv with
-      | Some _ -> msb.msb_equiv
-      | None -> Some mp 
-    end ;
-    msb_constraints = msb.msb_constraints; }
-
+and strengthen_mtb env mp mtb =
+  let mtb1 = eval_struct env mtb in 
+  match  mtb1 with
+  | SEBfunctor _ -> mtb1
+  | SEBstruct (msid,sign) -> 
+      SEBstruct (msid,strengthen_sig env msid sign mp)
+  | _ -> anomaly "Modops:the evaluation of the structure failed "
+
+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_retroknowledge = mb.mod_retroknowledge}
+      
 and strengthen_sig env msid sign mp = match sign with
   | [] -> []
-  | (l,SPBconst cb) :: rest ->
-      let item' = l,SPBconst (strengthen_const env mp l cb) in
+  | (l,SFBconst cb) :: rest ->
+      let item' = l,SFBconst (strengthen_const env mp l cb) in
       let rest' = strengthen_sig env msid rest mp in
 	item'::rest'
-  | (l,SPBmind mib) :: rest ->
-      let item' = l,SPBmind (strengthen_mind env mp l mib) in
+  | (l,SFBmind mib) :: rest ->
+      let item' = l,SFBmind (strengthen_mind env mp l mib) in
       let rest' = strengthen_sig env msid rest mp in
 	item'::rest'
-  | (l,SPBmodule mb) :: rest ->
+  | (l,SFBmodule mb) :: rest ->
       let mp' = MPdot (mp,l) in
-      let item' = l,SPBmodule (strengthen_mod env mp' mb) in
+      let item' = l,SFBmodule (strengthen_mod env mp' mb) in
       let env' = add_module 
 		   (MPdot (MPself msid,l)) 
-		   (module_body_of_spec mb) 
-		   env
+		   mb 
+		   env 
       in
       let rest' = strengthen_sig env' msid rest mp in
 	item'::rest'
-  | (l,SPBmodtype mty as item) :: rest -> 
+  | (l,SFBmodtype mty as item) :: rest -> 
       let env' = add_modtype 
-		   (make_kn (MPself msid) empty_dirpath l) 
-		   mty
+		   (MPdot((MPself msid),l)) 
+		   (mty,None)
 		   env
       in
       let rest' = strengthen_sig env' msid rest mp in
 	item::rest'
 
+    
 let strengthen env mtb mp = strengthen_mtb env mp mtb
+  
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index d7cdb59ac..3cb8e47bb 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -20,55 +20,52 @@ open Mod_subst
 
 (* Various operations on modules and module types *)
 
-(* recursively unfold MTBdent module types *)
-val scrape_modtype : env -> module_type_body -> module_type_body
-
 (* make the environment entry out of type *)
-val module_body_of_type : module_type_body -> module_body
-
-val module_body_of_spec : module_specification_body -> module_body 
-
-val module_spec_of_body : module_body -> module_specification_body
+val module_body_of_type : struct_expr_body -> module_body
 
 
 val destr_functor : 
-  module_type_body -> mod_bound_id * module_type_body * module_type_body
+  env -> struct_expr_body -> mod_bound_id * struct_expr_body * struct_expr_body
 
-
-val subst_modtype : substitution -> module_type_body -> module_type_body
+val subst_modtype : substitution -> struct_expr_body -> struct_expr_body
 
 val subst_signature_msid :
   mod_self_id -> module_path -> 
-  module_signature_body -> module_signature_body
+  structure_body -> structure_body
+
+(* Evaluation functions *)
+val eval_struct : env -> struct_expr_body -> struct_expr_body
+
+val type_of_mb : env -> module_body -> struct_expr_body
 
 (* [add_signature mp sign env] assumes that the substitution [msid]
    $\mapsto$ [mp] has already been performed (or is not necessary, like
    when [mp = MPself msid]) *)
 val add_signature : 
-  module_path -> module_signature_body -> env -> env
+  module_path -> structure_body -> env -> env
 
 (* adds a module and its components, but not the constraints *)
 val add_module :
-  module_path -> module_body ->  env -> env
+  module_path -> module_body -> env -> env
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
-val strengthen : env -> module_type_body -> module_path -> module_type_body
+val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body
 
 val error_existing_label : label -> 'a
 
-val error_declaration_not_path : module_expr -> 'a
+val error_declaration_not_path : module_struct_entry -> 'a
 
-val error_application_to_not_path : module_expr -> 'a
+val error_application_to_not_path : module_struct_entry -> 'a
 
-val error_not_a_functor : module_expr -> 'a
+val error_not_a_functor :  module_struct_entry -> 'a
 
 val error_incompatible_modtypes : 
-  module_type_body -> module_type_body -> 'a
+    struct_expr_body -> struct_expr_body -> 'a
 
 val error_not_equal : module_path -> module_path -> 'a
 
-val error_not_match : label -> specification_body -> 'a
+val error_not_match : label -> structure_field_body -> 'a
   
 val error_incompatible_labels : label -> label -> 'a
 
@@ -76,7 +73,7 @@ val error_no_such_label : label -> 'a
 
 val error_result_must_be_signature : unit -> 'a
 
-val error_signature_expected : module_type_body -> 'a
+val error_signature_expected : struct_expr_body -> 'a
 
 val error_no_module_to_end : unit -> 'a 
 
@@ -99,4 +96,4 @@ val error_local_context : label option -> 'a
 val error_no_such_label_sub : label->string->string->'a
 
 val resolver_of_environment :
- mod_bound_id -> module_type_body -> module_path -> env -> resolver
+  mod_bound_id -> struct_expr_body -> module_path -> env -> resolver
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 4f2498dc3..2b41e5a36 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -26,7 +26,7 @@ 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 KNmap.t }
+  env_modtypes : module_type_body MPmap.t }
 
 type stratification = {
   env_universes : universes;
@@ -60,7 +60,7 @@ let empty_env = {
     env_constants = Cmap.empty;
     env_inductives = KNmap.empty;
     env_modules = MPmap.empty;
-    env_modtypes = KNmap.empty };
+    env_modtypes = 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 511f56e65..b6d83b918 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -26,7 +26,7 @@ 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 KNmap.t }
+  env_modtypes : module_type_body MPmap.t }
 
 type stratification = {
   env_universes : universes;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f7f6a980d..368879713 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -28,8 +28,8 @@ open Mod_typing
 
 type modvariant = 
   | NONE 
-  | SIG of (* funsig params *) (mod_bound_id * module_type_body) list 
-  | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
+  | SIG of (* funsig params *) (mod_bound_id * struct_expr_body) list 
+  | STRUCT of (* functor params *) (mod_bound_id * struct_expr_body) list
   | LIBRARY of dir_path
 
 type module_info = 
@@ -54,8 +54,7 @@ type safe_environment =
       env : env;
       modinfo : module_info;
       labset : Labset.t;
-      revsign : module_signature_body;
-      revstruct : module_structure_body;
+      revstruct : structure_body;
       univ : Univ.constraints;
       engagement : engagement option;
       imports : library_info list;
@@ -84,7 +83,6 @@ let rec empty_environment =
       label = mk_label "_";
       variant = NONE};
     labset = Labset.empty;
-    revsign = [];
     revstruct = [];
     univ = Univ.Constraint.empty;
     engagement = None;
@@ -214,8 +212,7 @@ let add_constant dir l decl senv =
 	  env = env'';
 	  modinfo = senv.modinfo;
 	  labset = Labset.add l senv.labset;
-	  revsign = (l,SPBconst cb)::senv.revsign;
-	  revstruct = (l,SEBconst cb)::senv.revstruct;
+	  revstruct = (l,SFBconst cb)::senv.revstruct;
           univ = senv.univ;
           engagement = senv.engagement;
 	  imports = senv.imports;
@@ -244,8 +241,7 @@ let add_mind dir l mie senv =
 	env = env'';
 	modinfo = senv.modinfo;
 	labset = Labset.add l senv.labset;  (* TODO: the same as above *)
-	revsign = (l,SPBmind mib)::senv.revsign;
-	revstruct = (l,SEBmind mib)::senv.revstruct;
+	revstruct = (l,SFBmind mib)::senv.revstruct;
         univ = senv.univ;
         engagement = senv.engagement;
 	imports = senv.imports;
@@ -257,16 +253,15 @@ let add_mind dir l mie senv =
 
 let add_modtype l mte senv = 
   check_label l senv.labset; 
-  let mtb = translate_modtype senv.env mte in
+  let mtb = translate_struct_entry senv.env mte  in
   let env' = add_modtype_constraints senv.env mtb in
-  let kn = make_kn senv.modinfo.modpath empty_dirpath l in
-  let env'' = Environ.add_modtype kn mtb env' in
-  kn, { old = senv.old;
+  let mp = MPdot(senv.modinfo.modpath, l) in
+  let env'' = Environ.add_modtype mp (mtb,None) env' in
+  mp, { old = senv.old;
 	env = env'';
 	modinfo = senv.modinfo;
 	labset = Labset.add l senv.labset;
-	revsign = (l,SPBmodtype mtb)::senv.revsign;
-	revstruct = (l,SEBmodtype mtb)::senv.revstruct;
+	revstruct = (l,SFBmodtype mtb)::senv.revstruct;
         univ = senv.univ;
         engagement = senv.engagement;
 	imports = senv.imports;
@@ -285,15 +280,13 @@ let full_add_module mp mb env =
 let add_module l me senv = 
   check_label l senv.labset; 
   let mb = translate_module senv.env me in
-  let mspec = module_spec_of_body mb in
   let mp = MPdot(senv.modinfo.modpath, l) in
   let env' = full_add_module mp mb senv.env in
   mp, { old = senv.old;
 	env = env';
 	modinfo = senv.modinfo;
 	labset = Labset.add l senv.labset;
-	revsign = (l,SPBmodule mspec)::senv.revsign;
-	revstruct = (l,SEBmodule mb)::senv.revstruct;
+	revstruct = (l,SFBmodule mb)::senv.revstruct;
         univ = senv.univ;
         engagement = senv.engagement;
 	imports = senv.imports;
@@ -317,7 +310,6 @@ let start_module l senv =
 	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
-	revsign = [];
 	revstruct = [];
         univ = Univ.Constraint.empty;
         engagement = None;
@@ -329,7 +321,7 @@ let start_module l senv =
 let end_module l restype senv = 
   let oldsenv = senv.old in
   let modinfo = senv.modinfo in
-  let restype = Option.map (translate_modtype senv.env) restype in
+  let restype = Option.map (translate_struct_entry senv.env) restype in
   let params = 
     match modinfo.variant with
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
@@ -337,40 +329,32 @@ let end_module l restype senv =
   in
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_local_context None;
-  let functorize_type tb = 
+  let functorize_struct tb = 
     List.fold_left
-      (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb))
+      (fun mtb (arg_id,arg_b) -> 
+	SEBfunctor(arg_id,arg_b,mtb))
       tb
       params
   in
-  let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
-  let mtb, mod_user_type, cst = 
+   let auto_tb = 
+     SEBstruct (modinfo.msid, List.rev senv.revstruct)
+  in
+  let mod_typ, cst = 
     match restype with
-      | None -> functorize_type auto_tb, None, Constraint.empty
+      | None ->  None, Constraint.empty
       | Some res_tb -> 
 	  let cst = check_subtypes senv.env auto_tb res_tb in
-	  let mtb = functorize_type res_tb in
-	    mtb, Some mtb, cst
+	  let mtb = functorize_struct res_tb in
+	    Some mtb, cst
   in
+  let mexpr = functorize_struct auto_tb in
   let cst = Constraint.union cst senv.univ in
-  let mexpr = 
-    List.fold_left
-      (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb))
-      (MEBstruct (modinfo.msid, List.rev senv.revstruct)) 
-      params
-  in
   let mb = 
     { mod_expr = Some mexpr;
-      mod_user_type = mod_user_type;
-      mod_type = mtb;
+      mod_type = mod_typ;
       mod_equiv = None;
       mod_constraints = cst;
-      mod_retroknowledge = senv.local_retroknowledge}
-  in
-  let mspec = 
-    { msb_modtype = mtb;
-      msb_equiv = None;
-      msb_constraints = Constraint.empty } 
+      mod_retroknowledge = senv.local_retroknowledge }
   in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
@@ -388,8 +372,7 @@ let end_module l restype senv =
 	env = newenv;
 	modinfo = oldsenv.modinfo;
 	labset = Labset.add l oldsenv.labset;
-	revsign = (l,SPBmodule mspec)::oldsenv.revsign;
-	revstruct = (l,SEBmodule mb)::oldsenv.revstruct;
+	revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
         univ = oldsenv.univ;
         (* engagement is propagated to the upper level *)
         engagement = senv.engagement;
@@ -398,12 +381,85 @@ let end_module l restype senv =
 	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 = { senv with env = add_modtype_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" )
+   in
+   let mp_sup = senv.modinfo.modpath in
+   let str1 = subst_signature_msid msid mp_sup str 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 env' = Environ.add_constraints cb.const_constraints senv.env in
+	   let env'' = Environ.add_constant con cb env' in
+	     { old = senv.old;
+	       env = env'';
+	       modinfo = senv.modinfo;
+	       labset = Labset.add l senv.labset;
+	       revstruct = (l,SFBconst cb)::senv.revstruct;
+               univ = senv.univ;
+               engagement = senv.engagement;
+	       imports = senv.imports;
+	       loads = senv.loads ;
+	       local_retroknowledge = senv.local_retroknowledge }
+	       	     
+       | SFBmind mib ->
+	   let kn = make_kn mp_sup empty_dirpath l in
+	   let env' = Environ.add_constraints mib.mind_constraints senv.env in
+	   let env'' = Environ.add_mind kn mib env' in
+	     { old = senv.old;
+	       env = env'';
+	       modinfo = senv.modinfo;
+	       labset = Labset.add l senv.labset;  
+	       revstruct = (l,SFBmind mib)::senv.revstruct;
+               univ = senv.univ;
+               engagement = senv.engagement;
+	       imports = senv.imports;
+	       loads = senv.loads;
+               local_retroknowledge = senv.local_retroknowledge }
+	       
+       | SFBmodule mb ->
+	   let mp = MPdot(senv.modinfo.modpath, l) in
+	   let env' = full_add_module mp mb senv.env in
+	     { old = senv.old;
+	       env = env';
+	       modinfo = senv.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 }       
+       | 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
+	     { 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 }
+   in
+     List.fold_left add senv str1
+	   
 (* Adding parameters to modules or module types *)
 
 let add_module_parameter mbid mte senv =
-  if senv.revsign <> [] or senv.revstruct <> [] or senv.loads <> [] then
+  if  senv.revstruct <> [] or senv.loads <> [] then
     anomaly "Cannot add a module parameter to a non empty module";
-  let mtb = translate_modtype senv.env mte in
+  let mtb = translate_struct_entry senv.env mte in
   let env = full_add_module (MPbound mbid) (module_body_of_type mtb) senv.env 
   in
   let new_variant = match senv.modinfo.variant with
@@ -416,7 +472,6 @@ let add_module_parameter mbid mte senv =
     env = env;
     modinfo = { senv.modinfo with variant = new_variant };
     labset = senv.labset;
-    revsign = [];
     revstruct = [];
     univ = senv.univ;
     engagement = senv.engagement;
@@ -441,12 +496,11 @@ let start_modtype l senv =
 	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
-	revsign = [];
 	revstruct = [];
         univ = Univ.Constraint.empty;
         engagement = None;
 	imports = senv.imports;
-	loads = [];
+	loads = [] ;
 	(* spiwack: not 100% sure, but I think it should be like that *)
         local_retroknowledge = []}
 
@@ -460,14 +514,17 @@ let end_modtype l senv =
   in
   if l <> modinfo.label then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_local_context None;
-  let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in
+  let auto_tb = 
+     SEBstruct (modinfo.msid, List.rev senv.revstruct)
+  in
   let mtb = 
     List.fold_left
-      (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb))
-      res_tb
+      (fun mtb (arg_id,arg_b) -> 
+	 SEBfunctor(arg_id,arg_b,mtb))
+      auto_tb
       params
   in
-  let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l 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 *)
@@ -483,14 +540,13 @@ let end_modtype l senv =
     add_modtype_constraints newenv mtb 
   in
   let newenv = 
-    Environ.add_modtype kn mtb newenv
+    Environ.add_modtype mp (mtb,None) newenv
   in 
-  kn, { old = oldsenv.old;
+  mp, { old = oldsenv.old;
 	env = newenv;
 	modinfo = oldsenv.modinfo;
 	labset = Labset.add l oldsenv.labset;
-	revsign = (l,SPBmodtype mtb)::oldsenv.revsign;
-	revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct;
+	revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
         univ = Univ.Constraint.union senv.univ oldsenv.univ;
         engagement = senv.engagement;
 	imports = senv.imports;
@@ -532,7 +588,7 @@ type compiled_library =
    [start_library] was called *)
 
 let is_empty senv =
-  senv.revsign = [] &&
+  senv.revstruct = [] &&
   senv.modinfo.msid = initial_msid &&
   senv.modinfo.variant = NONE
 
@@ -557,7 +613,6 @@ let start_library dir senv =
 	env = senv.env;
 	modinfo = modinfo;
 	labset = Labset.empty;
-	revsign = [];
 	revstruct = [];
         univ = Univ.Constraint.empty;
         engagement = None;
@@ -567,7 +622,6 @@ let start_library dir senv =
 
 
 
-
 let export senv dir = 
   let modinfo = senv.modinfo in
   begin
@@ -581,9 +635,8 @@ let export senv dir =
   (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then
     (* error_export_simple *) (); *)
   let mb = 
-    { mod_expr = Some (MEBstruct (modinfo.msid, List.rev senv.revstruct));
-      mod_type = MTBsig (modinfo.msid, List.rev senv.revsign);
-      mod_user_type = None;
+    { mod_expr = Some (SEBstruct (modinfo.msid, List.rev senv.revstruct));
+      mod_type = None;
       mod_equiv = None;
       mod_constraints = senv.univ;
       mod_retroknowledge = senv.local_retroknowledge}
@@ -630,48 +683,31 @@ let import (dp,mb,depends,engmt) digest senv =
 
 
 (* Remove the body of opaque constants in modules *)
- 
-let rec lighten_module mb =
+ let rec lighten_module mb =
   { mb with
     mod_expr = Option.map lighten_modexpr mb.mod_expr;
-    mod_type = lighten_modtype mb.mod_type;
-    mod_user_type = Option.map lighten_modtype mb.mod_user_type }
-
-and lighten_modtype = function
-  | MTBident kn as x -> x
-  | MTBfunsig (mbid,mtb1,mtb2) ->
-      MTBfunsig (mbid, lighten_modtype mtb1, lighten_modtype mtb2)
-  | MTBsig (msid,sign) -> MTBsig (msid, lighten_sig sign)
-
-and lighten_modspec ms =
-  { ms with msb_modtype = lighten_modtype ms.msb_modtype }
-
-and lighten_sig sign = 
-  let lighten_spec (l,spec) = (l,match spec with
-    | SPBconst ({const_opaque=true} as x) -> SPBconst {x with const_body=None}
-    | (SPBconst _ | SPBmind _) as x -> x
-    | SPBmodule m -> SPBmodule (lighten_modspec m)
-    | SPBmodtype m -> SPBmodtype (lighten_modtype m))
-  in
-    List.map lighten_spec sign
-
+    mod_type = Option.map lighten_modexpr mb.mod_type;
+  }
+    
 and lighten_struct struc = 
   let lighten_body (l,body) = (l,match body with
-    | SEBconst ({const_opaque=true} as x) -> SEBconst {x with const_body=None}
-    | (SEBconst _ | SEBmind _) as x -> x
-    | SEBmodule m -> SEBmodule (lighten_module m)
-    | SEBmodtype m -> SEBmodtype (lighten_modtype m))
+    | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None}
+    | (SFBconst _ | SFBmind _) as x -> x
+    | SFBmodule m -> SFBmodule (lighten_module m)
+    | SFBmodtype m -> SFBmodtype (lighten_modexpr m))
   in
     List.map lighten_body struc
 
 and lighten_modexpr = function
-  | MEBfunctor (mbid,mty,mexpr) ->
-      MEBfunctor (mbid,lighten_modtype mty,lighten_modexpr mexpr)
-  | MEBident mp as x -> x
-  | MEBstruct (msid, struc) ->
-      MEBstruct (msid, lighten_struct struc)
-  | MEBapply (mexpr,marg,u) ->
-      MEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u)
+  | SEBfunctor (mbid,mty,mexpr) ->
+      SEBfunctor (mbid,lighten_modexpr mty,lighten_modexpr mexpr)
+  | SEBident mp as x -> x
+  | SEBstruct (msid, struc) ->
+      SEBstruct (msid, lighten_struct struc)
+  | SEBapply (mexpr,marg,u) ->
+      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 fe028c073..e764312b5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -59,8 +59,8 @@ val add_module :
 
 (* Adding a module type *)
 val add_modtype :
-  label -> module_type_entry -> safe_environment 
-    -> kernel_name * safe_environment
+  label -> module_struct_entry -> safe_environment 
+    -> module_path * safe_environment
 
 (* Adding universe constraints *)
 val add_constraints : 
@@ -73,20 +73,21 @@ val set_engagement : engagement -> safe_environment -> safe_environment
 (*s Interactive module functions *)
 val start_module : 
   label -> safe_environment -> module_path * safe_environment
-
 val end_module :
-  label -> module_type_entry option 
+  label -> module_struct_entry option 
       -> safe_environment -> module_path * safe_environment 
 
 val add_module_parameter :
-  mod_bound_id -> module_type_entry -> safe_environment -> safe_environment
+  mod_bound_id -> module_struct_entry -> safe_environment -> safe_environment
 
 val start_modtype :
   label -> safe_environment -> module_path * safe_environment
 
 val end_modtype :
-  label -> safe_environment -> kernel_name * safe_environment
+  label -> safe_environment -> module_path * safe_environment
 
+val add_include :
+  module_struct_entry -> safe_environment -> safe_environment
 
 val current_modpath : safe_environment -> module_path
 val current_msid : safe_environment -> mod_self_id
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index a9403a5e3..3db187a0b 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -27,13 +27,12 @@ open Entries
 (* This local type is used to subtype a constant with a constructor or
    an inductive type. It can also be useful to allow reorderings in
    inductive types *)
-
 type namedobject = 
   | Constant of constant_body
   | IndType of inductive * mutual_inductive_body
   | IndConstr of constructor * mutual_inductive_body
-  | Module of module_specification_body
-  | Modtype of module_type_body
+  | Module of module_body
+  | Modtype of struct_expr_body
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
@@ -59,11 +58,11 @@ let make_label_map mp list =
   let add_one (l,e) map = 
    let add_map obj = Labmap.add l obj map in
    match e with
-    | SPBconst cb -> add_map (Constant cb)
-    | SPBmind mib ->
+    | SFBconst cb -> add_map (Constant cb)
+    | SFBmind mib ->
        add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
-    | SPBmodule mb -> add_map (Module mb)
-    | SPBmodtype mtb -> add_map (Modtype mtb)
+    | SFBmodule mb -> add_map (Module mb)
+    | SFBmodtype mtb -> add_map (Modtype mtb)
   in
     List.fold_right add_one list Labmap.empty
 
@@ -290,10 +289,10 @@ 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 msb1.msb_modtype mp in
-  let cst = check_modtypes cst env mty1 msb2.msb_modtype false in
-  begin
-    match msb1.msb_equiv, msb2.msb_equiv with
+  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
@@ -316,18 +315,18 @@ and check_signatures cst env (msid1,sig1) (msid2,sig2') =
 	  Not_found -> error_no_such_label_sub l (string_of_msid msid1) (string_of_msid msid2)
     in
       match spec2 with
-	| SPBconst cb2 ->
+	| SFBconst cb2 ->
 	    check_constant cst env msid1 l info1 cb2 spec2
-	| SPBmind mib2 -> 
+	| SFBmind mib2 -> 
 	    check_inductive cst env msid1 l info1 mib2 spec2
-	| SPBmodule msb2 -> 
+	| SFBmodule msb2 -> 
 	    let msb1 = 
 	      match info1 with
 		| Module msb -> msb
 		| _ -> error_not_match l spec2
 	    in
 	      check_modules cst env msid1 l msb1 msb2
-	| SPBmodtype mtb2 ->
+	| SFBmodtype mtb2 ->
 	    let mtb1 = 
 	      match info1 with
 		| Modtype mtb -> mtb
@@ -339,19 +338,19 @@ and check_signatures cst env (msid1,sig1) (msid2,sig2') =
     
 and check_modtypes cst env mtb1 mtb2 equiv = 
   if mtb1==mtb2 then cst else (* just in case  :) *)
-  let mtb1' = scrape_modtype env mtb1 in
-  let mtb2' = scrape_modtype env mtb2 in
+  let mtb1' = eval_struct env mtb1 in
+  let mtb2' = eval_struct env mtb2 in
     if mtb1'==mtb2' then cst else
     match mtb1', mtb2' with
-      | MTBsig (msid1,list1), 
-	MTBsig (msid2,list2) -> 
+      | 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
-      | MTBfunsig (arg_id1,arg_t1,body_t1), 
-	MTBfunsig (arg_id2,arg_t2,body_t2) ->
+      | 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 = 
@@ -365,8 +364,6 @@ and check_modtypes cst env mtb1 mtb2 equiv =
 	      body_t1
 	  in
 	  check_modtypes cst env body_t1' body_t2 equiv
-      | MTBident _ , _ -> anomaly "Subtyping: scrape failed"
-      | _ , MTBident _ -> anomaly "Subtyping: scrape failed"
       | _ , _ -> error_incompatible_modtypes mtb1 mtb2
 	  
 let check_subtypes env sup super = 
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index c0b1ee5d3..d7288fc06 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -14,6 +14,6 @@ open Declarations
 open Environ
 (*i*)
 
-val check_subtypes : env -> module_type_body -> module_type_body -> constraints
+val check_subtypes : env -> struct_expr_body -> struct_expr_body -> constraints