Declarations.mli: reorganization of modular structures

 The earlier type [struct_expr_body] was far too broad,
 leading to code with unclear invariants, many "assert false", etc etc.
 Its replacement [module_alg_expr] has only three constructors:
   * MEident
   * MEapply : note the module_path as 2nd arg, no more constraints here
   * MEwith : no more constant_body inside, constr is just fine
 But no more SEBfunctor or SEBstruct constructor here (see below).
 This way, this datatype corresponds to algebraic expressions,
 i.e. anything that can appear in non-interactive modules.
 In fact, it even coincides now with [Entries.module_struct_entry].

 - Functor constructors are now necessarily on top of other
   structures thanks to a generic [functorize] datatype.

 - Structures are now separated from algebraic expressions by design :
   the [mod_type] and [typ_expr] fields now only contain structures
   (or functorized structures), while [mod_type_alg] and [typ_expr_alg]
   are restricted to algebraic expressions only.

 - Only the implementation field [mod_expr] could be either algebraic
   or structural. We handle this via a specialized datatype
   [module_implementation] with four constructors:

    * Abstract : no implementation (cf. for instance Declare Module)
    * Algebraic(_) : for non-interactive modules, e.g. Module M := N.
    * Struct(_) : for interactive module, e.g. Module M : T. ... End M.
    * FullStruct : for interactive module with no type restriction.

   The [FullStruct] is a particular case of [Struct] where the implementation
   need not be stored at all, since it is exactly equal to its expanded
   type present in [mod_type]. This is less fragile than hoping as earlier
   that pointer equality between [mod_type] and [mod_expr] will be
   preserved...

 - We clearly emphasize that only [mod_type] and [typ_expr] are
   relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
   are there only for a nicer extraction and shorter module printing.
   [mod_expr] is also not accessed by the kernel, but it is important
   for Print Assumptions later.

 - A few implicit invariants remain, for instance "no MEwith in mod_expr",
   see the final comment in Declarations

 - Heavy refactoring of module-related files : modops, mod_typing,
   safe_typing, declaremods, extraction/extract_env.ml ...

 - Coqchk has been adapted accordingly. The code concerning MEwith
   in Mod_checking is now gone, since we cannot have any in mod_expr.

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

31 files changed, 1402 insertions, 1791 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index fd3351674..0b732e4b9 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -276,8 +276,30 @@ type mutual_inductive_body = {
     mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
   }
 
-(** {6 Modules: signature component specifications, module types, and
-  module declarations } *)
+(** {6 Module declarations } *)
+
+(** Functor expressions are forced to be on top of other expressions *)
+
+type ('ty,'a) functorize =
+  | NoFunctor of 'a
+  | MoreFunctor of MBId.t * 'ty * ('ty,'a) functorize
+
+(** The fully-algebraic module expressions : names, applications, 'with ...'.
+    They correspond to the user entries of non-interactive modules.
+    They will be later expanded into module structures in [Mod_typing],
+    and won't play any role into the kernel after that : they are kept
+    only for short module printing and for extraction. *)
+
+type with_declaration =
+  | WithMod of Id.t list * module_path
+  | WithDef of Id.t list * constr
+
+type module_alg_expr =
+  | MEident of module_path
+  | MEapply of module_alg_expr * module_path
+  | MEwith of module_alg_expr * with_declaration
+
+(** A component of a module structure *)
 
 type structure_field_body =
   | SFBconst of constant_body
@@ -285,45 +307,51 @@ type structure_field_body =
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
 
-and structure_body = (label * structure_field_body) list
+(** A module structure is a list of labeled components.
+
+    Note : we may encounter now (at most) twice the same label in
+    a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
+    and once for an object ([SFBconst] or [SFBmind]) *)
+
+and structure_body = (Label.t * structure_field_body) list
+
+(** A module signature is a structure, with possibly functors on top of it *)
+
+and module_signature = (module_type_body,structure_body) functorize
+
+(** A module expression is an algebraic expression, possibly functorized. *)
+
+and module_expression = (module_type_body,module_alg_expr) functorize
 
-and struct_expr_body =
-  | SEBident of module_path
-  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
-  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
-  | SEBstruct of structure_body
-  | SEBwith of struct_expr_body * with_declaration_body
+and module_implementation =
+  | Abstract (** no accessible implementation *)
+  | Algebraic of module_expression (** non-interactive algebraic expression *)
+  | Struct of module_signature (** interactive body *)
+  | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
-and with_declaration_body =
-    With_module_body of Id.t list * module_path
-  | With_definition_body of  Id.t list * constant_body
 and module_body =
-    {  (** absolute path of the module *)
-      mod_mp : module_path;
-      (** Implementation *)
-      mod_expr : struct_expr_body option;
-      (** Signature *)
-      mod_type : struct_expr_body;
-      (** algebraic structure expression is kept
-	 if it's relevant for extraction  *)
-      mod_type_alg : struct_expr_body option;
-      (** set of all constraint in the module  *)
-      mod_constraints : Univ.constraints;
-      (** quotiented set of equivalent constant and inductive name  *)
-      mod_delta : delta_resolver;
-      mod_retroknowledge : action list}
+  { mod_mp : module_path; (** absolute path of the module *)
+    mod_expr : module_implementation; (** implementation *)
+    mod_type : module_signature; (** expanded type *)
+    (** algebraic type, kept if it's relevant for extraction *)
+    mod_type_alg : module_expression option;
+    (** set of all constraints in the module  *)
+    mod_constraints : Univ.constraints;
+    (** quotiented set of equivalent constants and inductive names *)
+    mod_delta : delta_resolver;
+    mod_retroknowledge : action list }
+
+(** A [module_type_body] is similar to a [module_body], with
+    no implementation and retroknowledge fields *)
 
 and module_type_body =
-    {
-      (** Path of the module type *)
-      typ_mp : module_path;
-      typ_expr : struct_expr_body;
-      (** algebraic structure expression is kept
-	 if it's relevant for extraction  *)
-      typ_expr_alg : struct_expr_body option ;
-      typ_constraints : Univ.constraints;
-      (** quotiented set of equivalent constant and inductive name  *)
-      typ_delta : delta_resolver}
+  { typ_mp : module_path; (** path of the module type *)
+    typ_expr : module_signature; (** expanded type *)
+    (** algebraic expression, kept if it's relevant for extraction  *)
+    typ_expr_alg : module_expression option;
+    typ_constraints : Univ.constraints;
+    (** quotiented set of equivalent constants and inductive names *)
+    typ_delta : delta_resolver}
 
 
 (*************************************************************************)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 0981cfd1a..eec76ba39 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -529,71 +529,50 @@ let subst_mind sub mib =
 
 (* Modules *)
 
-let rec subst_with_body sub = function
-  | With_module_body(id,mp) ->
-      With_module_body(id,subst_mp sub mp)
-  | With_definition_body(id,cb) ->
-      With_definition_body( id,subst_const_body sub cb)
+let rec functor_map fty f0 = function
+  | NoFunctor a -> NoFunctor (f0 a)
+  | MoreFunctor (mbid,ty,e) -> MoreFunctor(mbid,fty ty,functor_map fty f0 e)
+
+let implem_map fs fa = function
+  | Struct s -> Struct (fs s)
+  | Algebraic a -> Algebraic (fa a)
+  | impl -> impl
+
+let subst_with_body sub = function
+  | WithMod(id,mp) -> WithMod(id,subst_mp sub mp)
+  | WithDef(id,c) -> WithDef(id,subst_mps sub c)
+
+let rec subst_expr sub = function
+  | MEident mp -> MEident (subst_mp sub mp)
+  | MEapply (me1,mp2)-> MEapply (subst_expr sub me1, subst_mp sub mp2)
+  | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd)
+
+let rec subst_expression sub me =
+  functor_map (subst_modtype sub) (subst_expr sub) me
+
+and subst_signature sub sign =
+  functor_map (subst_modtype sub) (subst_structure sub) sign
 
 and subst_modtype sub mtb=
-  let typ_expr' = subst_struct_expr sub mtb.typ_expr in
-  let typ_alg' = 
-    Option.smartmap 
-      (subst_struct_expr sub) mtb.typ_expr_alg in
-  let mp = subst_mp sub mtb.typ_mp
-  in
-    if typ_expr'==mtb.typ_expr && 
-      typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then
-	mtb
-    else
-      {mtb with 
-	 typ_mp = mp;
-	 typ_expr = typ_expr';
-	 typ_expr_alg = typ_alg'}
+  { mtb with
+    typ_mp = subst_mp sub mtb.typ_mp;
+    typ_expr = subst_signature sub mtb.typ_expr;
+    typ_expr_alg = Option.smartmap (subst_expression sub) mtb.typ_expr_alg }
 
-and subst_structure sub sign = 
+and subst_structure sub struc =
   let subst_body = function
-      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)
+    | 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
-
+  List.map (fun (l,b) -> (l,subst_body b)) struc
 
 and subst_module sub mb =
-  let mtb' = subst_struct_expr sub mb.mod_type in
-  let typ_alg' = Option.smartmap 
-    (subst_struct_expr sub ) mb.mod_type_alg in
-  let me' = Option.smartmap 
-    (subst_struct_expr sub) mb.mod_expr in
-  let mp = subst_mp sub mb.mod_mp in
-     if mtb'==mb.mod_type && mb.mod_expr == me' 
-       && mp == mb.mod_mp
-    then mb else
-      { mb with
-	  mod_mp = mp;
-	  mod_expr = me';
-	  mod_type_alg = typ_alg';
-	  mod_type=mtb'}
-
-and subst_struct_expr sub = function
-    | SEBident mp -> SEBident (subst_mp sub mp)
-    | SEBfunctor (mbid, mtb, meb') -> 
-	SEBfunctor(mbid,subst_modtype sub mtb
-		     ,subst_struct_expr sub meb')
-    | SEBstruct (str)->
-	SEBstruct( 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)
-
+  { mb with
+    mod_mp = subst_mp sub mb.mod_mp;
+    mod_expr =
+      implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr;
+    mod_type = subst_signature sub mb.mod_type;
+    mod_type_alg = Option.map (subst_expression sub) mb.mod_type_alg }
 
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 64234e8cd..ab74114d5 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -37,9 +37,7 @@ val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
 
 val subst_const_body : constant_body subst_fun
 val subst_mind : mutual_inductive_body subst_fun
-val subst_modtype : substitution -> module_type_body -> module_type_body
-val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
-val subst_structure : substitution -> structure_body -> structure_body
+val subst_signature :  substitution -> module_signature -> module_signature
 val subst_module : substitution -> module_body -> module_body
 
 val join : substitution -> substitution -> substitution
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 66f1194d3..b0f20da70 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -13,8 +13,7 @@ open Subtyping
 open Declarations
 open Environ
 
-(************************************************************************)
-(* Checking constants *)
+(** {6 Checking constants } *)
 
 let refresh_arity ar =
   let ctxt, hd = decompose_prod_assum ar in
@@ -43,339 +42,95 @@ let check_constant_declaration env kn cb =
         check_polymorphic_arity env ctxt par);
   add_constant kn cb env
 
-(************************************************************************)
-(* Checking modules *)
 
+(** {6 Checking modules } *)
 
-exception Not_path
-
-let path_of_mexpr = function
-  | SEBident mp -> mp
-  | _ -> raise Not_path
-
-let is_modular = function
-  | SFBmodule _ | SFBmodtype _ -> true
-  | SFBconst _ | SFBmind _ -> false
-
-let rec list_split_assoc ((k,m) as km) rev_before = function
-  | [] -> raise Not_found
-  | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
-  | h::tail -> list_split_assoc km (h::rev_before) tail
-
-let check_definition_sub env cb1 cb2 =
-  let check_type env t1 t2 =
-
-    (* If the type of a constant is generated, it may mention
-       non-variable algebraic universes that the general conversion
-       algorithm is not ready to handle. Anyway, generated types of
-       constants are functions of the body of the constant. If the
-       bodies are the same in environments that are subtypes one of
-       the other, the types are subtypes too (i.e. if Gamma <= Gamma',
-       Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
-       Hence they don't have to be checked again *)
-
-    let t1,t2 =
-      if isArity t2 then
-        let (ctx2,s2) = destArity t2 in
-        match s2 with
-        | Type v when not (Univ.is_univ_variable v) ->
-          (* The type in the interface is inferred and is made of algebraic
-             universes *)
-          begin try
-            let (ctx1,s1) = dest_arity env t1 in
-            match s1 with
-            | Type u when not (Univ.is_univ_variable u) ->
-              (* Both types are inferred, no need to recheck them. We
-                 cheat and collapse the types to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Prop _ ->
-              (* The type in the interface is inferred, it may be the case
-                 that the type in the implementation is smaller because
-                 the body is more reduced. We safely collapse the upper
-                 type to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Type _ ->
-              (* The type in the interface is inferred and the type in the
-                 implementation is not inferred or is inferred but from a
-                 more reduced body so that it is just a variable. Since
-                 constraints of the form "univ <= max(...)" are not
-                 expressible in the system of algebraic universes: we fail
-                 (the user has to use an explicit type in the interface *)
-                raise Reduction.NotConvertible
-          with UserError _ (* "not an arity" *) ->
-            raise Reduction.NotConvertible end
-        | _ -> t1,t2
-      else
-        (t1,t2) in
-    Reduction.conv_leq env t1 t2
-  in
-  (*Start by checking types*)
-  let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-  let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-  check_type env typ1 typ2;
-  (* In the spirit of subtyping.check_constant, we accept
-     any implementations of parameters and opaques terms,
-     as long as they have the right type *)
-  (match cb2.const_body with
-    | Undef _ | OpaqueDef _ -> ()
-    | Def lc2 ->
-	(match cb1.const_body with
-	  | Def lc1 ->
-	    let c1 = force_constr lc1 in
-            let c2 = force_constr lc2 in
-	    Reduction.conv env c1 c2
-	  (* Coq only places transparent cb in With_definition_body *)
-	  | _ -> assert false))
-
-let lookup_modtype mp env =
-  try Environ.lookup_modtype mp env
-  with Not_found ->
-    failwith ("Unknown module type: "^string_of_mp mp)
+(** We currently ignore the [mod_type_alg] and [typ_expr_alg] fields.
+    The only delicate part is when [mod_expr] is an algebraic expression :
+    we need to expand it before checking it is indeed a subtype of [mod_type].
+    Fortunately, [mod_expr] cannot contain any [MEwith]. *)
 
 let lookup_module mp env =
   try Environ.lookup_module mp env
   with Not_found ->
     failwith ("Unknown module: "^string_of_mp mp)
 
-let rec check_with env mtb with_decl mp=
-  match with_decl with
-    | With_definition_body (idl,c) ->
-	check_with_def env mtb (idl,c) mp;
-	mtb
-    | With_module_body (idl,mp1) ->
-	check_with_mod env mtb (idl,mp1) mp;
-	mtb
-
-and check_with_def env mtb (idl,c) mp =
-  let sig_b = match mtb with
-    | SEBstruct(sig_b) ->
-	sig_b
-    | _ -> error_signature_expected mtb
+let rec check_module env mp mb =
+  let (_:module_signature) =
+    check_signature env mb.mod_type mb.mod_mp mb.mod_delta
   in
-  let id,idl = match idl with
-    | [] -> assert false
-    | id::idl -> id,idl
+  let optsign = match mb.mod_expr with
+    |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta)
+    |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta)
+    |Abstract|FullStruct -> None
   in
-  let l = Label.of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before empty_delta_resolver env in
-      if idl = [] then
-	      let cb = match spec with
-		  SFBconst cb -> cb
-		| _ -> error_not_a_constant l
-	      in
-              check_definition_sub env' c cb
-      else
-	      let old = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module l
-	      in
-		begin
-		  match old.mod_expr with
-                    | None ->
-		        check_with_def env' old.mod_type (idl,c) (MPdot(mp,l))
-                    | Some msb ->
-			error_a_generative_module_expected l
-		end
-    with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
-
-and check_with_mod env mtb (idl,mp1) mp =
-  let sig_b =
-    match mtb with
-    | SEBstruct(sig_b) ->
-	sig_b
-    | _ -> error_signature_expected mtb in
-  let id,idl = match idl with
-    | [] -> assert false
-    | id::idl -> id,idl
-  in
-  let l = Label.of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before empty_delta_resolver env in
-      if idl = [] then
-	      let _ = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module l
-	      in
-	      let (_:module_body) = (Environ.lookup_module mp1 env) in ()
-      else
-	    let old = match spec with
-		SFBmodule msb -> msb
-	      | _ -> error_not_a_module l
-	    in
-	      begin
-		match old.mod_expr with
-                    None ->
-		      check_with_mod env'
-			  old.mod_type (idl,mp1) (MPdot(mp,l))
-                  | Some msb ->
-                      error_a_generative_module_expected l
-              end
-    with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
+  match optsign with
+  |None -> ()
+  |Some sign ->
+    let mtb1 =
+      {typ_mp=mp;
+       typ_expr=sign;
+       typ_expr_alg=None;
+       typ_constraints=Univ.empty_constraint;
+       typ_delta = mb.mod_delta;}
+    and mtb2 =
+      {typ_mp=mp;
+       typ_expr=mb.mod_type;
+       typ_expr_alg=None;
+       typ_constraints=Univ.empty_constraint;
+       typ_delta = mb.mod_delta;}
+    in
+    let env = add_module_type mp mtb1 env in
+    Subtyping.check_subtypes env mtb1 mtb2
 
 and check_module_type env mty =
-  let (_:struct_expr_body) =
-    check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in
+  let (_:module_signature) =
+    check_signature env mty.typ_expr mty.typ_mp mty.typ_delta in
   ()
 
-							 
-and check_module env mp mb =
-  match mb.mod_expr, mb.mod_type with
-    | None,mtb -> 
-	let (_:struct_expr_body) =
-	  check_modtype env mtb mb.mod_mp mb.mod_delta in ()
-    | Some mexpr, mtb when mtb==mexpr ->
-	let (_:struct_expr_body) =
-	  check_modtype env mtb mb.mod_mp mb.mod_delta in ()
-    | Some mexpr, _ ->
-	let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
-	let (_:struct_expr_body) =
-	  check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
-	let mtb1 =
-	  {typ_mp=mp;
-	   typ_expr=sign;
-	   typ_expr_alg=None;
-	   typ_constraints=Univ.empty_constraint;
-	   typ_delta = mb.mod_delta;}
-	and mtb2 =
-	  {typ_mp=mp;
-	   typ_expr=mb.mod_type;
-	   typ_expr_alg=None;
-	   typ_constraints=Univ.empty_constraint;
-	   typ_delta = mb.mod_delta;}
-	in
-	let env = add_module (module_body_of_type mp mtb1) env in
-	check_subtypes env mtb1 mtb2
-
 and check_structure_field env mp lab res = function
   | SFBconst cb ->
       let c = Constant.make2 mp lab in
-	check_constant_declaration env c cb
+      check_constant_declaration env c cb
   | SFBmind mib ->
       let kn = MutInd.make2 mp lab in
       let kn = mind_of_delta res kn in
-	Indtypes.check_inductive env kn mib
+      Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
-      let (_:unit) = check_module env (MPdot(mp,lab)) msb in
-	Modops.add_module msb env
+      let () = check_module env (MPdot(mp,lab)) msb in
+      Modops.add_module msb env
   | SFBmodtype mty ->
       check_module_type env mty;
       add_modtype (MPdot(mp,lab)) mty env
-	
-and check_modexpr env mse mp_mse res = match mse with
-  | SEBident mp ->
+
+and check_mexpr env mse mp_mse res = match mse with
+  | MEident mp ->
       let mb = lookup_module mp env in
       (subst_and_strengthen mb mp_mse).mod_type
-  | SEBfunctor (arg_id, mtb, body) ->
-      check_module_type env mtb ;
-      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
-      let sign = check_modexpr env' body mp_mse res in
-	SEBfunctor (arg_id, mtb, sign)
-  | SEBapply (f,m,cst) ->
-      let sign = check_modexpr env f mp_mse res in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mp =
-	try (path_of_mexpr m)
-	with Not_path -> error_application_to_not_path m
-	  (* place for nondep_supertype *) in
-      let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
-	check_subtypes env mtb farg_b;
-	(subst_struct_expr (map_mbid farg_id mp) fbody_b)
-  | SEBwith(mte, with_decl) ->
-      let sign = check_modexpr env mte mp_mse res in
-      let sign = check_with env sign with_decl mp_mse in 
-	sign
-  | SEBstruct(msb) ->
-      let (_:env) = List.fold_left (fun env (lab,mb) ->
-		   check_structure_field env mp_mse lab res mb) env msb in
-	SEBstruct(msb)
-	
-and check_modtype env mse mp_mse res = match mse with
-  | SEBident mp ->
-      let mtb = lookup_modtype mp env in
-	mtb.typ_expr
-  | SEBfunctor (arg_id, mtb, body) ->
-      check_module_type env mtb;
-      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
-      let body = check_modtype env' body mp_mse res in
-	SEBfunctor(arg_id,mtb,body)
-  | SEBapply (f,m,cst) ->
-      let sign = check_modtype env f mp_mse res in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mp =
-	try (path_of_mexpr m)
-	with Not_path -> error_application_to_not_path m
-	  (* place for nondep_supertype *) in
+  | MEapply (f,mp) ->
+      let sign = check_mexpr env f mp_mse res in
+      let farg_id, farg_b, fbody_b = destr_functor sign in
       let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
-	check_subtypes env mtb farg_b;
-	subst_struct_expr (map_mbid farg_id mp) fbody_b
-  | SEBwith(mte, with_decl) ->
-      let sign = check_modtype env mte mp_mse res in
-      let sign = check_with env sign with_decl mp_mse in
-	sign
-  | SEBstruct(msb) ->
-      let (_:env) = List.fold_left (fun env (lab,mb) ->
-		   check_structure_field env mp_mse lab res mb) env msb in
-      SEBstruct(msb)
-	
-(*
-  let rec add_struct_expr_constraints env = function
-  | SEBident _ -> env
-  
-  | SEBfunctor (_,mtb,meb) ->
-  add_struct_expr_constraints
-  (add_modtype_constraints env mtb) meb
-
-  | SEBstruct (_,structure_body) ->
-      List.fold_left
-        (fun env (l,item) -> add_struct_elem_constraints env item)
-        env
-        structure_body
-
-  | SEBapply (meb1,meb2,cst) ->
-(*  let g = Univ.merge_constraints cst Univ.initial_universes in
-msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
-      Univ.pr_universes g++str"============="++fnl());
-*)
-      Environ.add_constraints cst
-        (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)
+      check_subtypes env mtb farg_b;
+      subst_signature (map_mbid farg_id mp) fbody_b
+  | MEwith _ -> error_with_module ()
 
-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 =
-  let env = match mb.mod_expr with
-    | None -> env
-    | Some meb -> add_struct_expr_constraints env meb
-  in
-  let env = match mb.mod_type with
-    | None -> env
-    | Some mtb ->
-	add_struct_expr_constraints env mtb
-  in
-    Environ.add_constraints mb.mod_constraints env
+and check_mexpression env sign mp_mse res = match sign with
+  | MoreFunctor (arg_id, mtb, body) ->
+      check_module_type env mtb;
+      let env' = add_module_type (MPbound arg_id) mtb env in
+      let body = check_mexpression env' body mp_mse res in
+      MoreFunctor(arg_id,mtb,body)
+  | NoFunctor me -> check_mexpr env me mp_mse res
 
-and add_modtype_constraints env mtb =
-  add_struct_expr_constraints env mtb.typ_expr
-*)
+and check_signature env sign mp_mse res = match sign with
+  | MoreFunctor (arg_id, mtb, body) ->
+      check_module_type env mtb;
+      let env' = add_module_type (MPbound arg_id) mtb env in
+      let body = check_signature env' body mp_mse res in
+      MoreFunctor(arg_id,mtb,body)
+  | NoFunctor struc ->
+      let (_:env) = List.fold_left (fun env (lab,mb) ->
+	check_structure_field env mp_mse lab res mb) env struc
+      in
+      NoFunctor struc
diff --git a/checker/modops.ml b/checker/modops.ml
index 20f330812..89ffcb50b 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -19,7 +19,7 @@ open Declarations
 let error_not_a_constant l =
   error ("\""^(Label.to_string l)^"\" is not a constant")
 
-let error_not_a_functor _ = error "Application of not a functor"
+let error_not_a_functor () = error "Application of not a functor"
 
 let error_incompatible_modtypes _ _ = error "Incompatible module types"
 
@@ -38,61 +38,52 @@ let error_not_a_module_loc loc s =
 
 let error_not_a_module s = error_not_a_module_loc Loc.ghost s
 
-let error_with_incorrect l =
-  error ("Incorrect constraint for label \""^(Label.to_string l)^"\"")
+let error_with_module () =
+  error "Unsupported 'with' constraint in module implementation"
 
-let error_a_generative_module_expected l =
-  error ("The module " ^ Label.to_string l ^ " is not generative. Only " ^
-         "component of generative modules can be changed using the \"with\" " ^
-         "construct.")
+let is_functor = function
+  | MoreFunctor _ -> true
+  | NoFunctor _ -> false
 
-let error_signature_expected mtb =
-  error "Signature expected"
+let destr_functor = function
+  | MoreFunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
+  | NoFunctor _ -> error_not_a_functor ()
 
-let error_application_to_not_path _ = error "Application to not path"
-
-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
-
-let module_body_of_type mp mtb = 
+let module_body_of_type mp mtb =
   { mod_mp = mp;
     mod_type = mtb.typ_expr;
     mod_type_alg = mtb.typ_expr_alg;
-    mod_expr = None;
+    mod_expr = Abstract;
     mod_constraints = mtb.typ_constraints;
     mod_delta = mtb.typ_delta;
     mod_retroknowledge = []}
 
-let rec add_signature mp sign resolver env = 
+let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
     let kn = KerName.make2 mp l in
     let con = Constant.make1 kn in
     let mind = mind_of_delta resolver (MutInd.make1 kn) in
       match elem with
-	| SFBconst cb -> 
+	| SFBconst cb ->
 	   (* let con =  constant_of_delta resolver con in*)
 	      Environ.add_constant con cb env
-	| SFBmind mib -> 
+	| SFBmind mib ->
 	   (* let mind =  mind_of_delta resolver mind in*)
 	    Environ.add_mind mind mib env
 	| SFBmodule mb -> add_module mb env
 	      (* adds components as well *)
 	| SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
   in
-    List.fold_left add_one env sign
+  List.fold_left add_one env sign
 
-and add_module mb env = 
+and add_module mb env =
   let mp = mb.mod_mp in
   let env = Environ.shallow_add_module mp mb env in
-    match mb.mod_type with
-      | SEBstruct (sign) -> 
-	    add_signature mp sign mb.mod_delta env
-      | SEBfunctor _ -> env
-      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
+  match mb.mod_type with
+  | NoFunctor struc -> add_structure mp struc mb.mod_delta env
+  | MoreFunctor _ -> env
 
+let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env
 
 let strengthen_const mp_from l cb resolver =
   match cb.const_body with
@@ -107,20 +98,20 @@ let rec strengthen_mod mp_from mp_to mb =
     mb
   else
     match mb.mod_type with
-     | SEBstruct (sign) -> 
-	 let resolve_out,sign_out = 
-	   strengthen_sig mp_from sign mp_to mb.mod_delta in
-	   { mb with
-	       mod_expr = Some (SEBident mp_to);
-	       mod_type = SEBstruct(sign_out);
-	       mod_type_alg = mb.mod_type_alg;
-	       mod_constraints = mb.mod_constraints;
-	       mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to 
-	       (add_delta_resolver mb.mod_delta resolve_out)*);
-	       mod_retroknowledge = mb.mod_retroknowledge}
-     | SEBfunctor _ -> mb
-     | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
-	 
+     | NoFunctor (sign) ->
+	 let resolve_out,sign_out =
+	   strengthen_sig mp_from sign mp_to mb.mod_delta
+         in
+	 { mb with
+	   mod_expr = Algebraic (NoFunctor (MEident mp_to));
+	   mod_type = NoFunctor sign_out;
+	   mod_type_alg = mb.mod_type_alg;
+	   mod_constraints = mb.mod_constraints;
+	   mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to
+	   (add_delta_resolver mb.mod_delta resolve_out)*);
+	   mod_retroknowledge = mb.mod_retroknowledge}
+     | MoreFunctor _ -> mb
+
 and strengthen_sig mp_from sign mp_to resolver =
   match sign with
     | [] -> empty_delta_resolver,[]
@@ -139,21 +130,20 @@ and strengthen_sig mp_from sign mp_to resolver =
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
 	resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
 	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest -> 
+    | (l,SFBmodtype mty as item) :: rest ->
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
 	resolve_out,item::rest'
 
-let strengthen mtb mp =
-    match mtb.typ_expr with
-      | SEBstruct (sign) -> 
-	  let resolve_out,sign_out =
-	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in
-	    {mtb with
-	       typ_expr = SEBstruct(sign_out);
-	       typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
-		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
-      | SEBfunctor _ -> mtb
-      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
+let strengthen mtb mp = match mtb.typ_expr with
+  | NoFunctor sign ->
+    let resolve_out,sign_out =
+      strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
+    in
+    { mtb with
+      typ_expr = NoFunctor sign_out;
+      typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
+      (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
+  | MoreFunctor _ -> mtb
 
 let subst_and_strengthen mb mp =
   strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
@@ -161,17 +151,16 @@ let subst_and_strengthen mb mp =
 
 let module_type_of_module mp mb =
   match mp with
-      Some mp ->
-	strengthen {
-	  typ_mp = mp;
-	  typ_expr = mb.mod_type;
-	  typ_expr_alg = None;
-	  typ_constraints = mb.mod_constraints;
-	  typ_delta = mb.mod_delta} mp
-	  
-    | None ->
-	{typ_mp = mb.mod_mp;
-	 typ_expr = mb.mod_type;
-	 typ_expr_alg = None;
-	 typ_constraints = mb.mod_constraints;
-	 typ_delta = mb.mod_delta}
+  | Some mp ->
+    strengthen {
+      typ_mp = mp;
+      typ_expr = mb.mod_type;
+      typ_expr_alg = None;
+      typ_constraints = mb.mod_constraints;
+      typ_delta = mb.mod_delta} mp
+  | None ->
+    { typ_mp = mb.mod_mp;
+      typ_expr = mb.mod_type;
+      typ_expr_alg = None;
+      typ_constraints = mb.mod_constraints;
+      typ_delta = mb.mod_delta}
diff --git a/checker/modops.mli b/checker/modops.mli
index 0b94edb54..396eb8e7c 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -15,20 +15,18 @@ open Environ
 
 (* Various operations on modules and module types *)
 
-(* make the envirconment entry out of type *)
-val module_body_of_type : module_path -> module_type_body -> module_body
+val module_type_of_module :
+  module_path option -> module_body -> module_type_body
 
-val module_type_of_module : module_path option -> module_body ->
-  module_type_body
+val is_functor : ('ty,'a) functorize -> bool
 
-val destr_functor :
-  env -> struct_expr_body -> MBId.t * module_type_body * struct_expr_body
-
-val add_signature : module_path -> structure_body -> delta_resolver -> env -> env
+val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize
 
 (* adds a module and its components, but not the constraints *)
 val add_module : module_body ->  env -> env
 
+val add_module_type : module_path -> module_type_body -> env -> env
+
 val strengthen : module_type_body -> module_path -> module_type_body
 
 val subst_and_strengthen : module_body -> module_path -> module_body
@@ -38,19 +36,13 @@ val error_incompatible_modtypes :
 
 val error_not_match : label -> structure_field_body -> 'a
 
-val error_with_incorrect : label -> 'a
+val error_with_module : unit -> 'a
 
 val error_no_such_label : label -> 'a
 
 val error_no_such_label_sub :
   label -> module_path -> 'a
 
-val error_signature_expected : struct_expr_body -> 'a
-
 val error_not_a_constant : label -> 'a
 
 val error_not_a_module : label -> 'a
-
-val error_a_generative_module_expected : label -> 'a
-
-val error_application_to_not_path : struct_expr_body -> 'a
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 150e99bc9..7903c33c5 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -320,55 +320,52 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
 		| Modtype mtb -> mtb
 		| _ -> error_not_match l spec2
 	    in
-	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
-	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
-	      check_modtypes  env mtb1 mtb2 subst1 subst2 true
+	    let env =
+              add_module_type mtb2.typ_mp mtb2
+	        (add_module_type mtb1.typ_mp mtb1 env)
+            in
+	    check_modtypes env mtb1 mtb2 subst1 subst2 true
   in
-    List.iter check_one_body sig2
+  List.iter check_one_body sig2
 
-and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv = 
-  if mtb1==mtb2 then () else 
-  let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
-  let rec check_structure  env str1 str2 equiv subst1 subst2 = 
-	match str1,str2 with
-	  | SEBstruct (list1), 
-	    SEBstruct (list2) -> 
-	       check_signatures env
-		mtb1.typ_mp list1 list2 subst1 subst2;
-		if equiv then
-		  check_signatures  env 
-		     mtb2.typ_mp list2 list1 subst1 subst2
-		else
-		  ()
-	  | SEBfunctor (arg_id1,arg_t1,body_t1),
-	      SEBfunctor (arg_id2,arg_t2,body_t2) ->
-	       check_modtypes env 
-		arg_t2 arg_t1
-		(map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
-		equiv ;
-		(* contravariant *)
-	      let env = add_module 
-		(module_body_of_type (MPbound arg_id2) arg_t2) env 
-	      in
-	      let env = match body_t1 with
-		  SEBstruct str ->
-		    let env = shallow_remove_module mtb1.typ_mp env in
-		    add_module {mod_mp = mtb1.typ_mp;
-				mod_expr = None;
-				mod_type = body_t1;
-				mod_type_alg= None;
-				mod_constraints=mtb1.typ_constraints;
-				mod_retroknowledge = [];
-				mod_delta = mtb1.typ_delta} env
-		| _ -> env
-	      in
-		check_structure env body_t1 body_t2 equiv 
-		  (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
-		  subst2
-	  | _ , _ -> error_incompatible_modtypes mtb1 mtb2
-      in
-     if mtb1'== mtb2' then ()
-     else check_structure  env mtb1' mtb2' equiv subst1 subst2
+and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
+  if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then ()
+  else
+    let rec check_structure  env str1 str2 equiv subst1 subst2 =
+      match str1,str2 with
+      | NoFunctor (list1),
+        NoFunctor (list2) ->
+	  check_signatures env mtb1.typ_mp list1 list2 subst1 subst2;
+	  if equiv then
+	    check_signatures env mtb2.typ_mp list2 list1 subst1 subst2
+	  else
+	    ()
+      | MoreFunctor (arg_id1,arg_t1,body_t1),
+	MoreFunctor (arg_id2,arg_t2,body_t2) ->
+	  check_modtypes env
+	    arg_t2 arg_t1
+	    (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
+	    equiv;
+	  (* contravariant *)
+	  let env = add_module_type (MPbound arg_id2) arg_t2 env in
+	  let env =
+            if is_functor body_t1 then env
+            else
+	      let env = shallow_remove_module mtb1.typ_mp env in
+	      add_module {mod_mp = mtb1.typ_mp;
+			  mod_expr = Abstract;
+			  mod_type = body_t1;
+			  mod_type_alg = None;
+			  mod_constraints = mtb1.typ_constraints;
+			  mod_retroknowledge = [];
+			  mod_delta = mtb1.typ_delta} env
+	  in
+	  check_structure env body_t1 body_t2 equiv
+	    (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
+	    subst2
+      | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+    in
+    check_structure env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2
 
 let check_subtypes env sup super =
   check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
diff --git a/checker/values.ml b/checker/values.ml
index 974d3431e..b39d90548 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 43e0b61e2a549058ae0a59bbadbb9d61 checker/cic.mli
+MD5 09a4e5d657809e040f50837a78fe6dfe checker/cic.mli
 
 *)
 
@@ -248,6 +248,18 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_cstrs;
     Any|]
 
+let v_with =
+  Sum ("with_declaration_body",0,
+       [|[|List v_id;v_mp|];
+         [|List v_id;v_constr|]|])
+
+let rec v_mae =
+  Sum ("module_alg_expr",0,
+  [|[|v_mp|];         (* SEBident *)
+    [|v_mae;v_mp|];   (* SEBapply *)
+    [|v_mae;v_with|]  (* SEBwith *)
+  |])
+
 let rec v_sfb =
   Sum ("struct_field_body",0,
   [|[|v_cb|];       (* SFBconst *)
@@ -255,27 +267,25 @@ let rec v_sfb =
     [|v_module|];   (* SFBmodule *)
     [|v_modtype|]   (* SFBmodtype *)
   |])
-and v_sb = List (Tuple ("label*sfb",[|v_id;v_sfb|]))
-and v_seb =
-  Sum ("struct_expr_body",0,
-  [|[|v_mp|];                  (* SEBident *)
-    [|v_uid;v_modtype;v_seb|]; (* SEBfunctor *)
-    [|v_seb;v_seb;v_cstrs|];   (* SEBapply *)
-    [|v_sb|];                  (* SEBstruct *)
-    [|v_seb;v_with|]           (* SEBwith *)
-  |])
-and v_with =
-  Sum ("with_declaration_body",0,
-       [|[|List v_id;v_mp|];
-         [|List v_id;v_cb|]|])
+and v_struc = List (Tuple ("label*sfb",[|v_id;v_sfb|]))
+and v_sign =
+  Sum ("module_sign",0,
+  [|[|v_struc|];                   (* NoFunctor *)
+    [|v_uid;v_modtype;v_sign|]|])  (* MoreFunctor *)
+and v_mexpr =
+  Sum ("module_expr",0,
+  [|[|v_mae|];                     (* NoFunctor *)
+    [|v_uid;v_modtype;v_mexpr|]|]) (* MoreFunctor *)
+and v_impl =
+  Sum ("module_impl",2,
+  [|[|v_mexpr|];  (* Algebraic *)
+    [|v_sign|]|])  (* Struct *)
 and v_module =
   Tuple ("module_body",
-         [|v_mp;Opt v_seb;v_seb;
-           Opt v_seb;v_cstrs;v_resolver;Any|])
+         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_seb;Opt v_seb;v_cstrs;v_resolver|])
-
+         [|v_mp;v_sign;Opt v_mexpr;v_cstrs;v_resolver|])
 
 (** kernel/safe_typing *)
 
diff --git a/interp/modintern.ml b/interp/modintern.ml
index d809f0221..8f8e2df93 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Declarations
 open Entries
 open Libnames
 open Constrexpr
@@ -59,34 +60,32 @@ let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
 
 let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
-      With_Module (fqid,lookup_module qid)
+      WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
-      With_Definition (fqid,interp_constr Evd.empty env c)
+      WithDef (fqid,interp_constr Evd.empty env c)
 
 let loc_of_module = function
   | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
 
-let is_path = function
-  | CMident _ -> true
-  | CMapply _ | CMwith _ -> false
-
 (* Invariant : the returned kind is never ModAny, and it is
    equal to the input kind when this one isn't ModAny. *)
 
 let rec interp_module_ast env kind = function
   | CMident qid ->
       let (mp,kind) = lookup_module_or_modtype kind qid in
-      (MSEident mp, kind)
+      (MEident mp, kind)
   | CMapply (_,me1,me2) ->
       let me1',kind1 = interp_module_ast env kind me1 in
       let me2',kind2 = interp_module_ast env ModAny me2 in
-      if not (is_path me2) then
-        error_application_to_not_path (loc_of_module me2) me2';
+      let mp2 = match me2' with
+        | MEident mp -> mp
+        | _ -> error_application_to_not_path (loc_of_module me2) me2'
+      in
       if kind2 == ModType then
         error_application_to_module_type (loc_of_module me2);
-      (MSEapply (me1',me2'), kind1)
+      (MEapply (me1',mp2), kind1)
   | CMwith (loc,me,decl) ->
       let me,kind = interp_module_ast env kind me in
       if kind == Module then error_incorrect_with_in_module loc;
       let decl = transl_with_decl env decl in
-      (MSEwith(me,decl), kind)
+      (MEwith(me,decl), kind)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 5cb406ffa..6a5b0dbb2 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -155,8 +155,30 @@ type mutual_inductive_body = {
 
   }
 
-(** {6 Modules: signature component specifications, module types, and
-  module declarations } *)
+(** {6 Module declarations } *)
+
+(** Functor expressions are forced to be on top of other expressions *)
+
+type ('ty,'a) functorize =
+  | NoFunctor of 'a
+  | MoreFunctor of MBId.t * 'ty * ('ty,'a) functorize
+
+(** The fully-algebraic module expressions : names, applications, 'with ...'.
+    They correspond to the user entries of non-interactive modules.
+    They will be later expanded into module structures in [Mod_typing],
+    and won't play any role into the kernel after that : they are kept
+    only for short module printing and for extraction. *)
+
+type with_declaration =
+  | WithMod of Id.t list * module_path
+  | WithDef of Id.t list * constr
+
+type module_alg_expr =
+  | MEident of module_path
+  | MEapply of module_alg_expr * module_path
+  | MEwith of module_alg_expr * with_declaration
+
+(** A component of a module structure *)
 
 type structure_field_body =
   | SFBconst of constant_body
@@ -164,47 +186,58 @@ type structure_field_body =
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
 
-(** NB: we may encounter now (at most) twice the same label in
+(** A module structure is a list of labeled components.
+
+    Note : we may encounter now (at most) twice the same label in
     a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
     and once for an object ([SFBconst] or [SFBmind]) *)
 
 and structure_body = (Label.t * structure_field_body) list
 
-and struct_expr_body =
-  | SEBident of module_path
-  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
-  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
-  | SEBstruct of structure_body
-  | SEBwith of struct_expr_body * with_declaration_body
+(** A module signature is a structure, with possibly functors on top of it *)
+
+and module_signature = (module_type_body,structure_body) functorize
+
+(** A module expression is an algebraic expression, possibly functorized. *)
 
-and with_declaration_body =
-    With_module_body of Id.t list * module_path
-  | With_definition_body of  Id.t list * constant_body
+and module_expression = (module_type_body,module_alg_expr) functorize
+
+and module_implementation =
+  | Abstract (** no accessible implementation *)
+  | Algebraic of module_expression (** non-interactive algebraic expression *)
+  | Struct of module_signature (** interactive body *)
+  | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
 and module_body =
-    {  (** absolute path of the module *)
-      mod_mp : module_path;
-      (** Implementation *)
-      mod_expr : struct_expr_body option;
-      (** Signature *)
-      mod_type : struct_expr_body;
-      (** algebraic structure expression is kept
-	 if it's relevant for extraction  *)
-      mod_type_alg : struct_expr_body option;
-      (** set of all constraint in the module  *)
-      mod_constraints : Univ.constraints;
-      (** quotiented set of equivalent constant and inductive name  *)
-      mod_delta : Mod_subst.delta_resolver;
-      mod_retroknowledge : Retroknowledge.action list}
+  { mod_mp : module_path; (** absolute path of the module *)
+    mod_expr : module_implementation; (** implementation *)
+    mod_type : module_signature; (** expanded type *)
+    (** algebraic type, kept if it's relevant for extraction *)
+    mod_type_alg : module_expression option;
+    (** set of all constraints in the module  *)
+    mod_constraints : Univ.constraints;
+    (** quotiented set of equivalent constants and inductive names *)
+    mod_delta : Mod_subst.delta_resolver;
+    mod_retroknowledge : Retroknowledge.action list }
+
+(** A [module_type_body] is similar to a [module_body], with
+    no implementation and retroknowledge fields *)
 
 and module_type_body =
-    {
-      (** Path of the module type *)
-      typ_mp : module_path;
-      typ_expr : struct_expr_body;
-      (** algebraic structure expression is kept
-	 if it's relevant for extraction  *)
-      typ_expr_alg : struct_expr_body option ;
-      typ_constraints : Univ.constraints;
-      (** quotiented set of equivalent constant and inductive name  *)
-      typ_delta : Mod_subst.delta_resolver}
+  { typ_mp : module_path; (** path of the module type *)
+    typ_expr : module_signature; (** expanded type *)
+    (** algebraic expression, kept if it's relevant for extraction  *)
+    typ_expr_alg : module_expression option;
+    typ_constraints : Univ.constraints;
+    (** quotiented set of equivalent constants and inductive names *)
+    typ_delta : Mod_subst.delta_resolver}
+
+(** Extra invariants :
+
+    - No [MEwith] inside a [mod_expr] implementation : the 'with' syntax
+      is only supported for module types
+
+    - A module application is atomic, for instance ((M N) P) :
+      * the head of [MEapply] can only be another [MEapply] or a [MEident]
+      * the argument of [MEapply] is now directly forced to be a [module_path].
+*)
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 3b7a2fd19..b78372c0e 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -67,16 +67,14 @@ type constant_entry =
 
 (** {6 Modules } *)
 
-type module_struct_entry =
-    MSEident of module_path
-  | MSEfunctor of MBId.t * 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 Id.t list * module_path
-  | With_Definition of Id.t list * constr
-
-and module_entry =
-    { mod_entry_type : module_struct_entry option;
-      mod_entry_expr : module_struct_entry option}
+type module_struct_entry = Declarations.module_alg_expr
+
+type module_params_entry =
+  (MBId.t * module_struct_entry) list (** older first *)
+
+type module_type_entry = module_params_entry * module_struct_entry
+
+type module_entry =
+  | MType of module_params_entry * module_struct_entry
+  | MExpr of
+      module_params_entry * module_struct_entry * module_struct_entry option
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index d5555c624..7794f19be 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -20,17 +20,13 @@ open Environ
 open Modops
 open Mod_subst
 
-exception Not_path
-
-let path_of_mexpr = function
-  | MSEident mp -> mp
-  | _ -> raise Not_path
+type 'alg translation =
+  module_signature * 'alg option * delta_resolver * Univ.constraints
 
 let rec mp_from_mexpr = function
-  | MSEident mp -> mp
-  | MSEapply (expr,_) -> mp_from_mexpr expr
-  | MSEfunctor (_,_,expr) -> mp_from_mexpr expr
-  | MSEwith (expr,_) -> mp_from_mexpr expr
+  | MEident mp -> mp
+  | MEapply (expr,_) -> mp_from_mexpr expr
+  | MEwith (expr,_) -> mp_from_mexpr expr
 
 let is_modular = function
   | SFBmodule _ | SFBmodtype _ -> true
@@ -39,7 +35,7 @@ let is_modular = function
 (** Split a [structure_body] at some label corresponding to
     a modular definition or not. *)
 
-let split_sign k m struc =
+let split_struc k m struc =
   let rec split rev_before = function
     | [] -> raise Not_found
     | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) ->
@@ -48,8 +44,8 @@ let split_sign k m struc =
   in split [] struc
 
 let discr_resolver mtb = match mtb.typ_expr with
-  | SEBstruct _ -> mtb.typ_delta
-  | _ -> empty_delta_resolver (* when mp is a functor *)
+  | NoFunctor _ -> mtb.typ_delta
+  | MoreFunctor _ -> empty_delta_resolver
 
 let rec rebuild_mp mp l =
   match l with
@@ -58,19 +54,15 @@ let rec rebuild_mp mp l =
 
 let (+++) = Univ.union_constraints
 
-let rec check_with_def env sign (idl,c) mp equiv =
-  let sig_b = match sign with
-    | SEBstruct(sig_b) -> sig_b
-    | _ -> error_signature_expected sign
-  in
+let rec check_with_def env struc (idl,c) mp equiv =
   let lab,idl = match idl with
     | [] -> assert false
     | id::idl -> Label.of_id id, idl
   in
   try
     let modular = not (List.is_empty idl) in
-    let before,spec,after = split_sign lab modular sig_b in
-    let env' = Modops.add_signature mp before equiv env in
+    let before,spec,after = split_struc lab modular struc in
+    let env' = Modops.add_structure mp before equiv env in
     if List.is_empty idl then
       (* Toplevel definition *)
       let cb = match spec with
@@ -80,27 +72,26 @@ let rec check_with_def env sign (idl,c) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 as long as they have the right type *)
-      let def,cst = match cb.const_body with
+      let c',cst = match cb.const_body with
 	| Undef _ | OpaqueDef _ ->
 	  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 = Future.force cb.const_constraints +++ cst1 +++ cst2 in
-	  let def = Def (Lazyconstr.from_val j.uj_val) in
-	  def,cst
+	  j.uj_val,cst
 	| Def cs ->
 	  let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
 	  let cst = Future.force cb.const_constraints +++ cst1 in
-	  let def = Def (Lazyconstr.from_val c) in
-	  def,cst
+          c, cst
       in
+      let def = Def (Lazyconstr.from_val c') in
       let cb' =
 	{ cb with
 	  const_body = def;
 	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
 	  const_constraints = Future.from_val cst }
       in
-      SEBstruct(before@(lab,SFBconst(cb'))::after),cb',cst
+      before@(lab,SFBconst(cb'))::after, c', cst
     else
       (* Definition inside a sub-module *)
       let mb = match spec with
@@ -108,33 +99,30 @@ let rec check_with_def env sign (idl,c) mp equiv =
 	| _ -> error_not_a_module (Label.to_string lab)
       in
       begin match mb.mod_expr with
-      | Some _ -> error_generative_module_expected lab
-      | None ->
-	let sign,cb,cst =
-          check_with_def env' mb.mod_type (idl,c) (MPdot(mp,lab)) mb.mod_delta
+      | Abstract ->
+        let struc = Modops.destr_nofunctor mb.mod_type in
+        let struc',c',cst =
+          check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta
         in
         let mb' = { mb with
-          mod_type = sign;
+          mod_type = NoFunctor struc';
 	  mod_type_alg = None }
         in
-	SEBstruct(before@(lab,SFBmodule mb')::after),cb,cst
+	before@(lab,SFBmodule mb')::after, c', cst
+      | _ -> error_generative_module_expected lab
       end
   with
   | Not_found -> error_no_such_label lab
   | Reduction.NotConvertible -> error_incorrect_with_constraint lab
 
-let rec check_with_mod env sign (idl,mp1) mp equiv =
-  let sig_b = match sign with
-    | SEBstruct(sig_b) -> sig_b
-    | _ -> error_signature_expected sign
-  in
+let rec check_with_mod env struc (idl,mp1) mp equiv =
   let lab,idl = match idl with
     | [] -> assert false
     | id::idl -> Label.of_id id, idl
   in
   try
-    let before,spec,after = split_sign lab true sig_b in
-    let env' = Modops.add_signature mp before equiv env in
+    let before,spec,after = split_struc lab true struc in
+    let env' = Modops.add_structure mp before equiv env in
     let old = match spec with
       | SFBmodule mb -> mb
       | _ -> error_not_a_module (Label.to_string lab)
@@ -142,33 +130,35 @@ let rec check_with_mod env sign (idl,mp1) mp equiv =
     if List.is_empty idl then
       (* Toplevel module definition *)
       let mb_mp1 = lookup_module mp1 env in
-      let mtb_mp1 = module_type_of_module None mb_mp1  in
+      let mtb_mp1 = module_type_of_module mb_mp1 in
       let cst = match old.mod_expr with
-	| None ->
+	| Abstract ->
 	  begin
             try
-              let mtb_old = module_type_of_module None old in
+              let mtb_old = module_type_of_module old in
               Subtyping.check_subtypes env' mtb_mp1 mtb_old
                 +++ old.mod_constraints
 	    with Failure _ -> error_incorrect_with_constraint lab
 	  end
-	| Some (SEBident(mp')) ->
+	| Algebraic (NoFunctor (MEident(mp'))) ->
 	  check_modpath_equiv env' mp1 mp';
 	  old.mod_constraints
-	| _ ->  error_generative_module_expected lab
+	| _ -> error_generative_module_expected lab
       in
       let mp' = MPdot (mp,lab) in
       let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in
-      let new_mb' = {new_mb with
-        mod_mp = mp';
-        mod_expr = Some (SEBident mp1);
-        mod_constraints = cst }
+      let new_mb' =
+        { new_mb with
+          mod_mp = mp';
+          mod_expr = Algebraic (NoFunctor (MEident mp1));
+          mod_constraints = cst }
       in
+      let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
       (* we propagate the new equality in the rest of the signature
 	 with the identity substitution accompagned by the new resolver*)
       let id_subst = map_mp mp' mp' new_mb.mod_delta in
-      SEBstruct(before@(lab,SFBmodule new_mb')::subst_signature id_subst after),
-      add_delta_resolver equiv new_mb.mod_delta,cst
+      let new_after = subst_structure id_subst after in
+      before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst
     else
       (* Module definition of a sub-module *)
       let mp' = MPdot (mp,lab) in
@@ -177,255 +167,163 @@ let rec check_with_mod env sign (idl,mp1) mp equiv =
 	| _ -> error_not_a_module (Label.to_string lab)
       in
       begin match old.mod_expr with
-      | None ->
-	let sign,equiv',cst =
-	  check_with_mod env' old.mod_type (idl,mp1) mp' old.mod_delta in
+      | Abstract ->
+        let struc = destr_nofunctor old.mod_type in
+	let struc',equiv',cst =
+          check_with_mod env' struc (idl,mp1) mp' old.mod_delta
+        in
+	let new_mb =
+          { old with
+            mod_type = NoFunctor struc';
+            mod_type_alg = None;
+            mod_delta = equiv' }
+        in
 	let new_equiv = add_delta_resolver equiv equiv' in
-	let new_mb = { old with
-          mod_type = sign;
-          mod_type_alg = None;
-          mod_delta = equiv'}
-	in
 	let id_subst = map_mp mp' mp' equiv' in
-	SEBstruct(before@(lab,SFBmodule new_mb)::subst_signature id_subst after),
-	new_equiv,cst
-      | Some (SEBident mp0) ->
+        let new_after = subst_structure id_subst after in
+	before@(lab,SFBmodule new_mb)::new_after, new_equiv, cst
+      | Algebraic (NoFunctor (MEident mp0)) ->
 	let mpnew = rebuild_mp mp0 idl in
 	check_modpath_equiv env' mpnew mp;
-	SEBstruct(before@(lab,spec)::after),equiv,Univ.empty_constraint
+	before@(lab,spec)::after, equiv, Univ.empty_constraint
       | _ -> error_generative_module_expected lab
       end
   with
   | Not_found -> error_no_such_label lab
   | Reduction.NotConvertible -> error_incorrect_with_constraint lab
 
-let check_with env sign with_decl alg_sign mp equiv =
-  let sign,wd,equiv,cst= match with_decl with
-    | With_Definition (idl,c) ->
-	let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
-	sign,With_definition_body(idl,cb),equiv,cst
-    | With_Module (idl,mp1) ->
-	let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
-	sign,With_module_body(idl,mp1),equiv,cst
-  in
-  match alg_sign with
-  | None -> sign, None, equiv, cst
-  | Some s -> sign, Some (SEBwith(s, wd)), equiv, cst
-
-let rec translate_module env mp inl me =
-  match me.mod_entry_expr, me.mod_entry_type with
-    | None, None ->
-	Errors.anomaly ~label:"Mod_typing.translate_module"
-          (Pp.str "empty type and expr in module entry")
-    | None, Some mte ->
-	let mtb = translate_module_type env mp inl mte in
-	  { mod_mp = mp;
-	    mod_expr = None;
-	    mod_type = mtb.typ_expr;
-	    mod_type_alg = mtb.typ_expr_alg;
-	    mod_delta = mtb.typ_delta;
-	    mod_constraints = mtb.typ_constraints; 
-	    mod_retroknowledge = []}
-   | Some mexpr, _ ->
-	let sign,alg_implem,resolver,cst1 =
-	  translate_struct_module_entry env mp inl mexpr in
-	let sign,alg1,resolver,cst2 =
-	  match me.mod_entry_type with
-	    | None ->
-		sign,None,resolver,Univ.empty_constraint
-	    | Some mte ->
-		let mtb = translate_module_type env mp inl mte in
-                let cst = Subtyping.check_subtypes env
-		  {typ_mp = mp;
-		   typ_expr = sign;
-		   typ_expr_alg = None;
-		   typ_constraints = Univ.empty_constraint;
-		   typ_delta = resolver;}
-		  mtb
-		in
-		  mtb.typ_expr,mtb.typ_expr_alg,mtb.typ_delta,cst
-	in
-	  { mod_mp = mp;
-	    mod_type = sign;
-	    mod_expr = alg_implem;
-	    mod_type_alg = alg1;
-	    mod_constraints = cst1 +++ cst2;
-	    mod_delta = resolver;
-	    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
-	       fix the bug.*)
-
-and translate_apply env inl ftrans mexpr mkalg =
-  let sign,alg,resolver,cst1 = ftrans in
+let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg
+
+let check_with env mp (sign,alg,reso,cst) = function
+  |WithDef(idl,c) ->
+    let struc = destr_nofunctor sign in
+    let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
+    let alg' = mk_alg_with alg (WithDef (idl,c')) in
+    (NoFunctor struc'),alg',reso, cst+++cst'
+  |WithMod(idl,mp1) as wd ->
+    let struc = destr_nofunctor sign in
+    let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
+    let alg' = mk_alg_with alg wd in
+    (NoFunctor struc'),alg',reso', cst+++cst'
+
+let mk_alg_app mpo alg arg = match mpo, alg with
+  | Some _, Some alg -> Some (MEapply (alg,arg))
+  | _ -> None
+
+(** Translation of a module struct entry :
+    - We translate to a module when a [module_path] is given,
+      otherwise to a module type.
+    - The first output is the expanded signature
+    - The second output is the algebraic expression, kept for the extraction.
+      It is never None when translating to a module, but for module type
+      it could not be contain [SEBapply] or [SEBfunctor].
+*)
+
+let rec translate_mse env mpo inl = function
+  |MEident mp1 ->
+    let sign,reso = match mpo with
+      |Some mp ->
+        let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
+        mb.mod_type, mb.mod_delta
+      |None ->
+        let mtb = lookup_modtype mp1 env in
+        mtb.typ_expr, mtb.typ_delta
+    in
+    sign,Some (MEident mp1),reso,Univ.empty_constraint
+  |MEapply (fe,mp1) ->
+    translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
+  |MEwith(me, with_decl) ->
+    assert (mpo == None); (* No 'with' syntax for modules *)
+    let mp = mp_from_mexpr me in
+    check_with env mp (translate_mse env None inl me) with_decl
+
+and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
   let farg_id, farg_b, fbody_b = destr_functor sign in
-  let mp1 =
-    try path_of_mexpr mexpr
-    with Not_path -> error_application_to_not_path mexpr
-  in
-  let mtb = module_type_of_module None (lookup_module mp1 env) in
+  let mtb = module_type_of_module (lookup_module mp1 env) in
   let cst2 = Subtyping.check_subtypes env mtb farg_b in
   let mp_delta = discr_resolver mtb in
   let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
   let subst = map_mbid farg_id mp1 mp_delta in
-  subst_struct_expr subst fbody_b,
-  mkalg alg mp1 cst2,
-  subst_codom_delta_resolver subst resolver,
-  cst1 +++ cst2
-
-and translate_functor env inl arg_id arg_e trans mkalg =
-  let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
-  let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
-  let sign,alg,resolver,cst = trans env'
+  let body = subst_signature subst fbody_b in
+  let alg' = mkalg alg mp1 in
+  let reso' = subst_codom_delta_resolver subst reso in
+  body,alg',reso', cst1 +++ cst2
+
+let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
+  | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
+  | _ -> None
+
+let rec translate_mse_funct env mpo inl mse = function
+  |[] ->
+    let sign,alg,reso,cst = translate_mse env mpo inl mse in
+    sign, Option.map (fun a -> NoFunctor a) alg, reso, cst
+  |(mbid, ty) :: params ->
+    let mp_id = MPbound mbid in
+    let mtb = translate_modtype env mp_id inl ([],ty) in
+    let env' = add_module_type mp_id mtb env in
+    let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
+    let alg' = mk_alg_funct mpo mbid mtb alg in
+    MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.typ_constraints
+
+and translate_modtype env mp inl (params,mte) =
+  let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
+  let mtb =
+    { typ_mp = mp_from_mexpr mte;
+      typ_expr = sign;
+      typ_expr_alg = None;
+      typ_constraints = cst;
+      typ_delta = reso }
   in
-  SEBfunctor (arg_id, mtb, sign),
-  mkalg alg arg_id mtb,
-  resolver,
-  cst +++ mtb.typ_constraints
-
-and translate_struct_module_entry env mp inl = function
-  | MSEident mp1 ->
-      let mb = lookup_module mp1 env in
-      let mb' = strengthen_and_subst_mb mb mp false in
-      mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint
-  | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let trans env' = translate_struct_module_entry env' mp inl body_expr in
-      let mkalg a id m = Option.map (fun a -> SEBfunctor (id,m,a)) a in
-      translate_functor env inl arg_id arg_e trans mkalg
-  | MSEapply (fexpr,mexpr) ->
-      let trans = translate_struct_module_entry env mp inl fexpr in
-      let mkalg a mp c = Option.map (fun a -> SEBapply(a,SEBident mp,c)) a in
-      translate_apply env inl trans mexpr mkalg
-  | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,cst1 =
-	translate_struct_module_entry env mp inl mte in
-      let sign,alg,resolve,cst2 =
-	check_with env sign with_decl alg mp resolve in
-      sign,alg,resolve, cst1 +++ cst2
-
-and translate_struct_type_entry env inl = function
-  | MSEident mp1 ->
-      let mtb = lookup_modtype mp1 env in
-      mtb.typ_expr,Some (SEBident mp1),mtb.typ_delta,Univ.empty_constraint
-  | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let trans env' = translate_struct_type_entry env' inl body_expr in
-      translate_functor env inl arg_id arg_e trans (fun _ _ _ -> None)
-  | MSEapply (fexpr,mexpr) ->
-      let trans = translate_struct_type_entry env inl fexpr in
-      translate_apply env inl trans mexpr (fun _ _ _ -> None)
-  | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,cst1 = translate_struct_type_entry env inl mte in
-      let sign,alg,resolve,cst2 =
-	check_with env sign with_decl alg (mp_from_mexpr mte) resolve
-      in
-      sign,alg,resolve, cst1 +++ cst2
-
-and translate_module_type env mp inl mte =
-  let mp_from = mp_from_mexpr mte in
-  let sign,alg,resolve,cst = translate_struct_type_entry env inl mte in
-  let mtb = subst_modtype_and_resolver
-    {typ_mp = mp_from;
-     typ_expr = sign;
-     typ_expr_alg = None;
-     typ_constraints = cst;
-     typ_delta = resolve} mp
-  in {mtb with typ_expr_alg = alg}
-
-let rec translate_struct_include_module_entry env mp inl = function
-  | MSEident mp1 ->
-      let mb = lookup_module mp1 env in
-      let mb' = strengthen_and_subst_mb mb mp true in
-      let mb_typ = clean_bounded_mod_expr mb'.mod_type in
-      mb_typ,None,mb'.mod_delta,Univ.empty_constraint
-  | MSEapply (fexpr,mexpr) ->
-      let ftrans = translate_struct_include_module_entry env mp inl fexpr in
-      translate_apply env inl ftrans mexpr (fun _ _ _ -> None)
-  | _ -> Modops.error_higher_order_include ()
-
-let rec add_struct_expr_constraints env = function
-  | SEBident _ -> env
-
-  | SEBfunctor (_,mtb,meb) ->
-      add_struct_expr_constraints
-	(add_modtype_constraints env mtb) meb
-
-  | SEBstruct (structure_body) ->
-      List.fold_left
-        (fun env (_,item) -> add_struct_elem_constraints env item)
-        env
-        structure_body
-
-  | SEBapply (meb1,meb2,cst) ->
-      Environ.add_constraints cst
-        (add_struct_expr_constraints
-	  (add_struct_expr_constraints env meb1)
-	  meb2)
-  | SEBwith(meb,With_definition_body(_,cb))->
-      Environ.add_constraints (Future.force cb.const_constraints)
-	(add_struct_expr_constraints env meb)
-  | SEBwith(meb,With_module_body(_,_))->
-      add_struct_expr_constraints env meb
-		
-and add_struct_elem_constraints env = function 
-  | SFBconst cb -> 
-      Environ.add_constraints (Future.force 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 =
-  let env = match mb.mod_expr with
-    | None -> env
-    | Some meb -> add_struct_expr_constraints env meb
-  in
-  let env =
-    add_struct_expr_constraints env mb.mod_type
-  in
-    Environ.add_constraints mb.mod_constraints env
-
-and add_modtype_constraints env mtb =
-  Environ.add_constraints mtb.typ_constraints
-    (add_struct_expr_constraints env mtb.typ_expr)
-
-
-let rec struct_expr_constraints cst = function
-  | SEBident _ -> cst
-
-  | SEBfunctor (_,mtb,meb) ->
-      struct_expr_constraints
-	(modtype_constraints cst mtb) meb
-
-  | SEBstruct (structure_body) ->
-      List.fold_left
-        (fun cst (_,item) -> struct_elem_constraints cst item)
-        cst
-        structure_body
-
-  | SEBapply (meb1,meb2,cst1) ->
-      struct_expr_constraints (struct_expr_constraints (cst1 +++ cst) meb1)
-        meb2
-  | SEBwith(meb,With_definition_body(_,cb))->
-      struct_expr_constraints ((Future.force cb.const_constraints) +++ cst) meb
-  | SEBwith(meb,With_module_body(_,_))->
-      struct_expr_constraints  cst meb
-
-and struct_elem_constraints cst = function
-  | SFBconst cb -> cst
-  | SFBmind mib -> cst
-  | SFBmodule mb -> module_constraints cst mb
-  | SFBmodtype mtb -> modtype_constraints cst mtb
-
-and module_constraints cst mb =
-  let cst = match mb.mod_expr with
-    | None -> cst
-    | Some meb -> struct_expr_constraints cst meb in
-  let cst = struct_expr_constraints cst mb.mod_type in
-  mb.mod_constraints +++ cst
-
-and modtype_constraints cst mtb =
-  struct_expr_constraints (mtb.typ_constraints +++ cst) mtb.typ_expr
-
-
-let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint
-let module_constraints = module_constraints Univ.empty_constraint
+  let mtb' = subst_modtype_and_resolver mtb mp in
+  { mtb' with typ_expr_alg = alg }
+
+(** [finalize_module] :
+    from an already-translated (or interactive) implementation
+    and a signature entry, produce a final [module_expr] *)
+
+let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
+  |None ->
+    let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
+    { mod_mp = mp;
+      mod_expr = impl;
+      mod_type = sign;
+      mod_type_alg = None;
+      mod_constraints = cst;
+      mod_delta = reso;
+      mod_retroknowledge = [] }
+  |Some (params_mte,inl) ->
+    let res_mtb = translate_modtype env mp inl params_mte in
+    let auto_mtb = {
+      typ_mp = mp;
+      typ_expr = sign;
+      typ_expr_alg = None;
+      typ_constraints = Univ.empty_constraint;
+      typ_delta = reso } in
+    let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
+    let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
+    { mod_mp = mp;
+      mod_expr = impl;
+      mod_type = res_mtb.typ_expr;
+      mod_type_alg = res_mtb.typ_expr_alg;
+      mod_constraints = cst +++ cst';
+      mod_delta = res_mtb.typ_delta;
+      mod_retroknowledge = [] }
+
+let translate_module env mp inl = function
+  |MType (params,ty) ->
+    let mtb = translate_modtype env mp inl (params,ty) in
+    module_body_of_type mp mtb
+  |MExpr (params,mse,oty) ->
+    let t = translate_mse_funct env (Some mp) inl mse params in
+    let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
+    finalize_module env mp t restype
+
+let rec translate_mse_incl env mp inl = function
+  |MEident mp1 ->
+    let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
+    let sign = clean_bounded_mod_expr mb.mod_type in
+    sign,None,mb.mod_delta,Univ.empty_constraint
+  |MEapply (fe,arg) ->
+    let ftrans = translate_mse_incl env mp inl fe in
+    translate_apply env inl ftrans arg (fun _ _ -> None)
+  |_ -> Modops.error_higher_order_include ()
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 0990e36c1..21171705d 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -12,40 +12,40 @@ open Entries
 open Mod_subst
 open Names
 
+(** Main functions for translating module entries
+
+    Note : [module_body] and [module_type_body] obtained this way
+    won't have any [MEstruct] in their algebraic fields.
+*)
 
 val translate_module :
   env -> module_path -> inline -> module_entry -> module_body
 
-val translate_module_type :
-  env -> module_path -> inline -> module_struct_entry -> module_type_body
+val translate_modtype :
+  env -> module_path -> inline -> module_type_entry -> module_type_body
 
-val translate_struct_module_entry :
-  env -> module_path -> inline -> module_struct_entry ->
-  struct_expr_body (* Signature *)
-  * struct_expr_body option  (* Algebraic expr, in fact never None *)
-  * delta_resolver
-  * Univ.constraints
-
-val translate_struct_type_entry :
-  env -> inline -> module_struct_entry ->
-  struct_expr_body
-  * struct_expr_body option
-  * delta_resolver
-  * Univ.constraints
-
-val translate_struct_include_module_entry :
-  env -> module_path -> inline -> module_struct_entry ->
-  struct_expr_body
-  * struct_expr_body option (* Algebraic expr, always None *)
-  * delta_resolver
-  * Univ.constraints
+(** Low-level function for translating a module struct entry :
+    - We translate to a module when a [module_path] is given,
+      otherwise to a module type.
+    - The first output is the expanded signature
+    - The second output is the algebraic expression, kept for the extraction.
+      It is never None when translating to a module, but for module type
+      it could not be contain applications or functors.
+      Moreover algebraic expressions obtained here cannot contain [MEstruct].
+*)
 
-val add_modtype_constraints : env -> module_type_body -> env
+type 'alg translation =
+  module_signature * 'alg option * delta_resolver * Univ.constraints
 
-val add_module_constraints : env -> module_body -> env
+val translate_mse :
+  env -> module_path option -> inline -> module_struct_entry ->
+    module_alg_expr translation
 
-val add_struct_expr_constraints : env -> struct_expr_body -> env
-
-val struct_expr_constraints : struct_expr_body -> Univ.constraints
+val translate_mse_incl :
+  env -> module_path -> inline -> module_struct_entry ->
+    module_alg_expr translation
 
-val module_constraints : module_body -> Univ.constraints
+val finalize_module :
+  env -> module_path -> module_expression translation ->
+  (module_type_entry * inline) option ->
+  module_body
diff --git a/kernel/modops.ml b/kernel/modops.ml
index deff291ec..76feb8498 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -51,12 +51,12 @@ type module_typing_error =
       Label.t * structure_field_body * signature_mismatch_error
   | LabelAlreadyDeclared of Label.t
   | ApplicationToNotPath of module_struct_entry
-  | NotAFunctor of struct_expr_body
+  | NotAFunctor
+  | IsAFunctor
   | IncompatibleModuleTypes of module_type_body * module_type_body
   | NotEqualModulePaths of module_path * module_path
   | NoSuchLabel of Label.t
   | IncompatibleLabels of Label.t * Label.t
-  | SignatureExpected of struct_expr_body
   | NotAModule of string
   | NotAModuleType of string
   | NotAConstant of Label.t
@@ -73,8 +73,11 @@ let error_existing_label l =
 let error_application_to_not_path mexpr =
   raise (ModuleTypingError (ApplicationToNotPath mexpr))
 
-let error_not_a_functor mtb =
-  raise (ModuleTypingError (NotAFunctor mtb))
+let error_not_a_functor () =
+  raise (ModuleTypingError NotAFunctor)
+
+let error_is_a_functor () =
+  raise (ModuleTypingError IsAFunctor)
 
 let error_incompatible_modtypes mexpr1 mexpr2 =
   raise (ModuleTypingError (IncompatibleModuleTypes (mexpr1,mexpr2)))
@@ -91,9 +94,6 @@ let error_no_such_label l =
 let error_incompatible_labels l l' =
   raise (ModuleTypingError (IncompatibleLabels (l,l')))
 
-let error_signature_expected mtb =
-  raise (ModuleTypingError (SignatureExpected mtb))
-
 let error_not_a_module s =
   raise (ModuleTypingError (NotAModule s))
 
@@ -112,24 +112,49 @@ let error_no_such_label_sub l l1 =
 let error_higher_order_include () =
   raise (ModuleTypingError HigherOrderInclude)
 
-(** {6 Misc operations } *)
+(** {6 Operations on functors } *)
+
+let is_functor = function
+  |NoFunctor _ -> false
+  |MoreFunctor _ -> true
 
 let destr_functor = function
-  | SEBfunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
-  | mtb -> error_not_a_functor mtb
+  |NoFunctor _ -> error_not_a_functor ()
+  |MoreFunctor (mbid,ty,x) -> (mbid,ty,x)
 
-let is_functor = function
-  | SEBfunctor _ -> true
-  | _ -> false
+let destr_nofunctor = function
+  |NoFunctor a -> a
+  |MoreFunctor _ -> error_is_a_functor ()
+
+let rec functor_smartmap fty f0 funct = match funct with
+  |MoreFunctor (mbid,ty,e) ->
+    let ty' = fty ty in
+    let e' = functor_smartmap fty f0 e in
+    if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e')
+  |NoFunctor a ->
+    let a' = f0 a in if a==a' then funct else NoFunctor a'
+
+let rec functor_iter fty f0 = function
+  |MoreFunctor (mbid,ty,e) -> fty ty; functor_iter fty f0 e
+  |NoFunctor a -> f0 a
+
+(** {6 Misc operations } *)
+
+let module_type_of_module mb =
+  { typ_mp = mb.mod_mp;
+    typ_expr = mb.mod_type;
+    typ_expr_alg = None;
+    typ_constraints = mb.mod_constraints;
+    typ_delta = mb.mod_delta }
 
 let module_body_of_type mp mtb =
   { mod_mp = mp;
     mod_type = mtb.typ_expr;
     mod_type_alg = mtb.typ_expr_alg;
-    mod_expr = None;
+    mod_expr = Abstract;
     mod_constraints = mtb.typ_constraints;
     mod_delta = mtb.typ_delta;
-    mod_retroknowledge = []}
+    mod_retroknowledge = [] }
 
 let check_modpath_equiv env mp1 mp2 =
   if ModPath.equal mp1 mp2 then ()
@@ -139,17 +164,27 @@ let check_modpath_equiv env mp1 mp2 =
     if ModPath.equal mp1' mp2' then ()
     else error_not_equal_modpaths mp1 mp2
 
+let implem_smartmap fs fa impl = match impl with
+  |Struct e -> let e' = fs e in if e==e' then impl else Struct e'
+  |Algebraic a -> let a' = fa a in if a==a' then impl else Algebraic a'
+  |Abstract|FullStruct -> impl
+
+let implem_iter fs fa impl = match impl with
+  |Struct e -> fs e
+  |Algebraic a -> fa a
+  |Abstract|FullStruct -> ()
+
 (** {6 Substitutions of modular structures } *)
 
 let id_delta x y = x
 
 let rec subst_with_body sub = function
-  |With_module_body(id,mp) as orig ->
+  |WithMod(id,mp) as orig ->
     let mp' = subst_mp sub mp in
-    if mp==mp' then orig else With_module_body(id,mp')
-  |With_definition_body(id,cb) as orig ->
-    let cb' = subst_const_body sub cb in
-    if cb==cb' then orig else With_definition_body(id,cb')
+    if mp==mp' then orig else WithMod(id,mp')
+  |WithDef(id,c) as orig ->
+    let c' = subst_mps sub c in
+    if c==c' then orig else WithDef(id,c')
 
 and subst_modtype sub do_delta mtb=
   let { typ_mp = mp; typ_expr = ty; typ_expr_alg = aty } = mtb in
@@ -158,8 +193,8 @@ and subst_modtype sub do_delta mtb=
     if ModPath.equal mp mp' then sub
     else add_mp mp mp' empty_delta_resolver sub
   in
-  let ty' = subst_struct_expr sub do_delta ty in
-  let aty' = Option.smartmap (subst_struct_expr sub id_delta) aty in
+  let ty' = subst_signature sub do_delta ty in
+  let aty' = Option.smartmap (subst_expression sub id_delta) aty in
   let delta' = do_delta mtb.typ_delta sub in
   if mp==mp' && ty==ty' && aty==aty' && delta'==mtb.typ_delta
   then mtb
@@ -172,16 +207,16 @@ and subst_modtype sub do_delta mtb=
 
 and subst_structure sub do_delta sign =
   let subst_body ((l,body) as orig) = match body with
-    | SFBconst cb ->
+    |SFBconst cb ->
       let cb' = subst_const_body sub cb in
       if cb==cb' then orig else (l,SFBconst cb')
-    | SFBmind mib ->
+    |SFBmind mib ->
       let mib' = subst_mind sub mib in
       if mib==mib' then orig else (l,SFBmind mib')
-    | SFBmodule mb ->
+    |SFBmodule mb ->
       let mb' = subst_module sub do_delta mb in
       if mb==mb' then orig else (l,SFBmodule mb')
-    | SFBmodtype mtb ->
+    |SFBmodtype mtb ->
       let mtb' = subst_modtype sub do_delta mtb in
       if mtb==mtb' then orig else (l,SFBmodtype mtb')
   in
@@ -194,13 +229,12 @@ and subst_module sub do_delta mb =
     if not (is_functor ty) || ModPath.equal mp mp' then sub
     else add_mp mp mp' empty_delta_resolver sub
   in
-  let ty' = subst_struct_expr sub do_delta ty in
-  (* Special optim : maintain sharing between [mod_expr] and [mod_type] *)
-  let me' = match me with
-    | Some m when m == ty -> if ty == ty' then me else Some ty'
-    | _ -> Option.smartmap (subst_struct_expr sub id_delta) me
+  let ty' = subst_signature sub do_delta ty in
+  let me' =
+    implem_smartmap
+      (subst_signature sub id_delta) (subst_expression sub id_delta) me
   in
-  let aty' = Option.smartmap (subst_struct_expr sub id_delta) aty in
+  let aty' = Option.smartmap (subst_expression sub id_delta) aty in
   let delta' = do_delta mb.mod_delta sub in
   if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta
   then mb
@@ -212,34 +246,35 @@ and subst_module sub do_delta mb =
       mod_type_alg = aty';
       mod_delta = delta' }
 
-and subst_struct_expr sub do_delta seb = match seb with
-  |SEBident mp ->
+and subst_expr sub do_delta seb = match seb with
+  |MEident mp ->
     let mp' = subst_mp sub mp in
-    if mp==mp' then seb else SEBident mp'
-  |SEBfunctor (mbid, mtb, meb) ->
-    let mtb' = subst_modtype sub do_delta mtb in
-    let meb' = subst_struct_expr sub do_delta meb in
-    if mtb==mtb' && meb==meb' then seb
-    else SEBfunctor(mbid,mtb',meb')
-  |SEBstruct str ->
-    let str' = subst_structure sub do_delta str in
-    if str==str' then seb else SEBstruct str'
-  |SEBapply (meb1,meb2,cst) ->
-    let meb1' = subst_struct_expr sub do_delta meb1 in
-    let meb2' = subst_struct_expr sub do_delta meb2 in
-    if meb1==meb1' && meb2==meb2' then seb else SEBapply(meb1',meb2',cst)
-  |SEBwith (meb,wdb) ->
-    let meb' = subst_struct_expr sub do_delta meb in
+    if mp==mp' then seb else MEident mp'
+  |MEapply (meb1,mp2) ->
+    let meb1' = subst_expr sub do_delta meb1 in
+    let mp2' = subst_mp sub mp2 in
+    if meb1==meb1' && mp2==mp2' then seb else MEapply(meb1',mp2')
+  |MEwith (meb,wdb) ->
+    let meb' = subst_expr sub do_delta meb in
     let wdb' = subst_with_body sub wdb in
-    if meb==meb' && wdb==wdb' then seb else SEBwith(meb',wdb')
+    if meb==meb' && wdb==wdb' then seb else MEwith(meb',wdb')
+
+and subst_expression sub do_delta =
+  functor_smartmap
+    (subst_modtype sub do_delta)
+    (subst_expr sub do_delta)
+
+and subst_signature sub do_delta =
+  functor_smartmap
+    (subst_modtype sub do_delta)
+    (subst_structure sub do_delta)
 
-let subst_signature subst =
-  subst_structure subst
-    (fun resolver subst-> subst_codom_delta_resolver subst resolver)
+let do_delta_dom reso sub = subst_dom_delta_resolver sub reso
+let do_delta_codom reso sub = subst_codom_delta_resolver sub reso
+let do_delta_dom_codom reso sub = subst_dom_codom_delta_resolver sub reso
 
-let subst_struct_expr subst =
-  subst_struct_expr subst
-    (fun resolver subst-> subst_codom_delta_resolver subst resolver)
+let subst_signature subst = subst_signature subst do_delta_codom
+let subst_structure subst = subst_structure subst do_delta_codom
 
 (** {6 Retroknowledge } *)
 
@@ -247,16 +282,12 @@ let subst_struct_expr subst =
    the retroknowledge declared in the library *)
 (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
 let add_retroknowledge mp =
-  let perform rkaction env =
-    match rkaction with
-      | Retroknowledge.RKRegister (f, e) ->
-	  Environ.register env f 
-	  (match e with 
-	    | Const kn -> kind_of_term (mkConst kn)
-	    | Ind ind -> kind_of_term (mkInd ind)
-	    | _ ->
-              anomaly ~label:"Modops.add_retroknowledge"
-                (Pp.str "had to import an unsupported kind of term"))
+  let perform rkaction env = match rkaction with
+    |Retroknowledge.RKRegister (f, (Const _ | Ind _ as e)) ->
+      Environ.register env f e
+    |_ ->
+      Errors.anomaly ~label:"Modops.add_retroknowledge"
+        (Pp.str "had to import an unsupported kind of term")
   in
   fun lclrk env ->
   (* The order of the declaration matters, for instance (and it's at the
@@ -271,7 +302,7 @@ let add_retroknowledge mp =
 
 (** {6 Adding a module in the environment } *)
 
-let rec add_signature mp sign resolver env =
+let rec add_structure mp sign resolver env =
   let add_one env (l,elem) = match elem with
     |SFBconst cb ->
       let c = constant_of_delta_kn resolver (KerName.make2 mp l) in
@@ -288,105 +319,71 @@ and add_module mb env =
   let mp = mb.mod_mp in
   let env = Environ.shallow_add_module mb env in
   match mb.mod_type with
-  | SEBstruct (sign) ->
+  |NoFunctor struc ->
     add_retroknowledge mp mb.mod_retroknowledge
-      (add_signature mp sign mb.mod_delta env)
-  | SEBfunctor _ -> env
-  | _ ->
-    anomaly ~label:"Modops"
-      (Pp.str "the evaluation of the structure failed ")
+      (add_structure mp struc mb.mod_delta env)
+  |MoreFunctor _ -> env
+
+let add_module_type mp mtb env =
+  add_module (module_body_of_type mp mtb) env
 
 (** {6 Strengtening } *)
 
 let strengthen_const mp_from l cb resolver =
   match cb.const_body with
-    | Def _ -> cb
-    | _ ->
-      let kn = KerName.make2 mp_from l in
-      let con = constant_of_delta_kn resolver kn in
-      { cb with
-	const_body = Def (Lazyconstr.from_val (mkConst con));
-	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con)
-      }
+  |Def _ -> cb
+  |_ ->
+    let kn = KerName.make2 mp_from l in
+    let con = constant_of_delta_kn resolver kn in
+    { cb with
+      const_body = Def (Lazyconstr.from_val (mkConst con));
+      const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) }
 
 let rec strengthen_mod mp_from mp_to mb =
-  if mp_in_delta mb.mod_mp mb.mod_delta then
-    mb
-  else
-    match mb.mod_type with
-     | SEBstruct (sign) ->
-	 let resolve_out,sign_out =
-           strengthen_sig mp_from sign mp_to mb.mod_delta
-         in
-	 { mb with
-	   mod_expr = Some (SEBident mp_to);
-	   mod_type = SEBstruct(sign_out);
-	   mod_type_alg = mb.mod_type_alg;
-	   mod_constraints = mb.mod_constraints;
-	   mod_delta = add_mp_delta_resolver mp_from mp_to
-	     (add_delta_resolver mb.mod_delta resolve_out);
-	   mod_retroknowledge = mb.mod_retroknowledge }
-     | SEBfunctor _ -> mb
-     | _ ->
-       anomaly ~label:"Modops"
-         (Pp.str "the evaluation of the structure failed ")
-
-and strengthen_sig mp_from sign mp_to resolver =
-  match sign with
-    | [] -> empty_delta_resolver,[]
-    | (l,SFBconst cb) :: rest ->
-	let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	resolve_out,item'::rest'
-    | (_,SFBmind _ as item):: rest ->
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	resolve_out,item::rest'
-    | (l,SFBmodule mb) :: rest ->
-	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot(mp_to,l) in
-	let mb_out = strengthen_mod mp_from' mp_to' mb in
-	let item' = l,SFBmodule (mb_out) in
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	add_delta_resolver resolve_out mb.mod_delta, item':: rest'
-    | (l,SFBmodtype mty as item) :: rest ->
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	resolve_out,item::rest'
+  if mp_in_delta mb.mod_mp mb.mod_delta then mb
+  else match mb.mod_type with
+  |NoFunctor struc ->
+    let reso,struc' = strengthen_sig mp_from struc mp_to mb.mod_delta in
+    { mb with
+      mod_expr = Algebraic (NoFunctor (MEident mp_to));
+      mod_type = NoFunctor struc';
+      mod_delta =
+        add_mp_delta_resolver mp_from mp_to
+	  (add_delta_resolver mb.mod_delta reso) }
+  |MoreFunctor _ -> mb
+
+and strengthen_sig mp_from struc mp_to reso = match struc with
+  |[] -> empty_delta_resolver,[]
+  |(l,SFBconst cb) :: rest ->
+    let item' = l,SFBconst (strengthen_const mp_from l cb reso) in
+    let reso',rest' = strengthen_sig mp_from rest mp_to reso in
+    reso',item'::rest'
+  |(_,SFBmind _ as item):: rest ->
+    let reso',rest' = strengthen_sig mp_from rest mp_to reso in
+    reso',item::rest'
+  |(l,SFBmodule mb) :: rest ->
+    let mp_from' = MPdot (mp_from,l) in
+    let mp_to' = MPdot(mp_to,l) in
+    let mb' = strengthen_mod mp_from' mp_to' mb in
+    let item' = l,SFBmodule mb' in
+    let reso',rest' = strengthen_sig mp_from rest mp_to reso in
+    add_delta_resolver reso' mb.mod_delta, item':: rest'
+  |(l,SFBmodtype mty as item) :: rest ->
+    let reso',rest' = strengthen_sig mp_from rest mp_to reso in
+    reso',item::rest'
 
 let strengthen mtb mp =
-  if mp_in_delta mtb.typ_mp mtb.typ_delta then
-    (* in this case mtb has already been strengthened*)
-    mtb
-  else
-    match mtb.typ_expr with
-      | SEBstruct (sign) ->
-	  let resolve_out,sign_out =
-	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
-          in
-	  {mtb with
-	    typ_expr = SEBstruct(sign_out);
-	    typ_delta = add_delta_resolver mtb.typ_delta
-	      (add_mp_delta_resolver mtb.typ_mp mp resolve_out)}
-      | SEBfunctor _ -> mtb
-      | _ ->
-        anomaly ~label:"Modops"
-          (Pp.str "the evaluation of the structure failed ")
-
-let module_type_of_module mp mb =
-  match mp with
-      Some mp ->
-	strengthen {
-	  typ_mp = mp;
-	  typ_expr = mb.mod_type;
-	  typ_expr_alg = None;
-	  typ_constraints = mb.mod_constraints;
-	  typ_delta = mb.mod_delta} mp
-
-    | None ->
-	{typ_mp = mb.mod_mp;
-	 typ_expr = mb.mod_type;
-	 typ_expr_alg = None;
-	 typ_constraints = mb.mod_constraints;
-	 typ_delta = mb.mod_delta}
+  (* Has mtb already been strengthened ? *)
+  if mp_in_delta mtb.typ_mp mtb.typ_delta then mtb
+  else match mtb.typ_expr with
+  |NoFunctor struc ->
+    let reso',struc' = strengthen_sig mtb.typ_mp struc mp mtb.typ_delta in
+    { mtb with
+      typ_expr = NoFunctor struc';
+      typ_delta =
+        add_delta_resolver mtb.typ_delta
+	  (add_mp_delta_resolver mtb.typ_mp mp reso') }
+  |MoreFunctor _ -> mtb
 
 let inline_delta_resolver env inl mp mbid mtb delta =
   let constants = inline_of_delta inl mtb.typ_delta in
@@ -409,109 +406,97 @@ let inline_delta_resolver env inl mp mbid mtb delta =
   in
   make_inline delta constants
 
-let rec strengthen_and_subst_mod mb subst mp_from mp_to resolver =
+let rec strengthen_and_subst_mod mb subst mp_from mp_to =
   match mb.mod_type with
-    | SEBstruct str ->
-      let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
-      if mb_is_an_alias then
-	subst_module subst
-	  (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb
-      else
-	let resolver,new_sig =
-	  strengthen_and_subst_struct str subst
-	    mp_from mp_from mp_to false false mb.mod_delta
-	in
-	{mb with
-	  mod_mp = mp_to;
-	  mod_expr = Some (SEBident mp_from);
-	  mod_type = SEBstruct(new_sig);
-	  mod_delta = add_mp_delta_resolver mp_to mp_from resolver}
-    | SEBfunctor(arg_id,arg_b,body) ->
-      let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
-      subst_module subst
-	(fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb
-    | _ ->
-      anomaly ~label:"Modops"
-        (Pp.str "the evaluation of the structure failed ")
-
-and strengthen_and_subst_struct
-    str subst mp_alias mp_from mp_to alias incl resolver =
+  |NoFunctor struc ->
+    let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
+    if mb_is_an_alias then subst_module subst do_delta_dom mb
+    else
+      let reso',struc' =
+	strengthen_and_subst_struct struc subst
+	  mp_from mp_to false false mb.mod_delta
+      in
+      { mb with
+	mod_mp = mp_to;
+	mod_expr = Algebraic (NoFunctor (MEident mp_from));
+	mod_type = NoFunctor struc';
+	mod_delta = add_mp_delta_resolver mp_to mp_from reso' }
+  |MoreFunctor _ ->
+    let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
+    subst_module subst do_delta_dom mb
+
+and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
   match str with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
-	let item' = if alias then 
-	  (* case alias no strengthening needed*)
-	  l,SFBconst (subst_const_body subst cb) 
-	else 
-	  l,SFBconst (strengthen_const mp_from l
-			(subst_const_body subst cb) resolver)
-	in
-	let resolve_out,rest' =
-	  strengthen_and_subst_struct rest subst
-	    mp_alias mp_from mp_to alias incl resolver in
+        let cb' = subst_const_body subst cb in
+        let cb'' =
+          if alias then cb'
+          else strengthen_const mp_from l cb' reso
+        in
+        let item' = l, SFBconst cb'' in
+	let reso',rest' =
+	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+        in
 	if incl then
-	    (* If we are performing an inclusion we need to add
-	       the fact that the constant mp_to.l is \Delta-equivalent
-	       to resolver(mp_from.l) *)
-	  let kn_from = KerName.make2 mp_from l in
-	  let kn_to = KerName.make2 mp_to l in
-	  let old_name = kn_of_delta resolver kn_from in
-	  (add_kn_delta_resolver kn_to old_name resolve_out),
-	  item'::rest'
+          (* If we are performing an inclusion we need to add
+             the fact that the constant mp_to.l is \Delta-equivalent
+             to reso(mp_from.l) *)
+          let kn_from = KerName.make2 mp_from l in
+          let kn_to = KerName.make2 mp_to l in
+          let old_name = kn_of_delta reso kn_from in
+	  add_kn_delta_resolver kn_to old_name reso', item'::rest'
 	else
-	    (*In this case the fact that the constant mp_to.l is 
-	      \Delta-equivalent to resolver(mp_from.l) is already known
-	       because resolve_out contains mp_to maps to resolver(mp_from)*)
-	  resolve_out,item'::rest'
+	  (* In this case the fact that the constant mp_to.l is
+	     \Delta-equivalent to resolver(mp_from.l) is already known
+	     because reso' contains mp_to maps to reso(mp_from) *)
+	  reso', item'::rest'
     | (l,SFBmind mib) :: rest ->
-	(*Same as constant*)
 	let item' = l,SFBmind (subst_mind subst mib) in
-	let resolve_out,rest' =
-	  strengthen_and_subst_struct rest subst
-	    mp_alias mp_from mp_to alias incl resolver in
+	let reso',rest' =
+	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+        in
+	(* Same as constant *)
 	if incl then
 	  let kn_from = KerName.make2 mp_from l in
 	  let kn_to = KerName.make2 mp_to l in
-	  let old_name = kn_of_delta resolver kn_from in
-	  (add_kn_delta_resolver kn_to old_name resolve_out),
-	  item'::rest'
+	  let old_name = kn_of_delta reso kn_from in
+	  add_kn_delta_resolver kn_to old_name reso', item'::rest'
 	else
-	  resolve_out,item'::rest'
+	  reso', item'::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot(mp_to,l) in
-	let mb_out = if alias then 
-	  subst_module subst 
-	  (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb 
+	let mp_to' = MPdot (mp_to,l) in
+	let mb' = if alias then
+	  subst_module subst do_delta_dom mb
 	else
-	  strengthen_and_subst_mod
-	    mb subst mp_from' mp_to' resolver
+	  strengthen_and_subst_mod mb subst mp_from' mp_to'
 	in
-	let item' = l,SFBmodule (mb_out) in
-	let resolve_out,rest' =
-	  strengthen_and_subst_struct rest subst
-	    mp_alias mp_from mp_to alias incl resolver in
-	  (* if mb is a functor we should not derive new equivalences
-	     on names, hence we add the fact that the functor can only
-	     be equivalent to itself. If we adopt an applicative
-	     semantic for functor this should be changed.*)
-	  if is_functor mb_out.mod_type then 
-	    (add_mp_delta_resolver 
-	       mp_to' mp_to' resolve_out),item':: rest' 
-	  else
-	    add_delta_resolver resolve_out mb_out.mod_delta,
-	item':: rest'
-    | (l,SFBmodtype mty) :: rest -> 
+	let item' = l,SFBmodule mb' in
+	let reso',rest' =
+	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+        in
+        (* if mb is a functor we should not derive new equivalences
+           on names, hence we add the fact that the functor can only
+           be equivalent to itself. If we adopt an applicative
+           semantic for functor this should be changed.*)
+	if is_functor mb'.mod_type then
+	  add_mp_delta_resolver mp_to' mp_to' reso', item':: rest'
+	else
+	  add_delta_resolver reso' mb'.mod_delta, item':: rest'
+    | (l,SFBmodtype mty) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot(mp_to,l) in
 	let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
-	let mty = subst_modtype subst' 
-	  (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in
-	let resolve_out,rest' = strengthen_and_subst_struct rest subst
-	    mp_alias mp_from mp_to alias incl resolver
+	let mty = subst_modtype subst'
+	  (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver)
+          mty
         in
-	(add_mp_delta_resolver mp_to' mp_to' resolve_out),
-        (l,SFBmodtype mty)::rest'
+        let item' = l,SFBmodtype mty in
+	let reso',rest' =
+          strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+        in
+	add_mp_delta_resolver mp_to' mp_to' reso', item'::rest'
 
 
 (** Let P be a module path when we write:
@@ -521,7 +506,7 @@ and strengthen_and_subst_struct
     - The second one is strenghtening. *)
 
 let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
-  |SEBstruct str ->
+  |NoFunctor struc ->
     let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
     (* if mb.mod_mp is an alias then the strengthening is useless
        (i.e. it is already done)*)
@@ -529,168 +514,125 @@ let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
     let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in
     let new_resolver =
       add_mp_delta_resolver mp mp_alias
-	(subst_dom_delta_resolver subst_resolver mb.mod_delta) in
+	(subst_dom_delta_resolver subst_resolver mb.mod_delta)
+    in
     let subst = map_mp mb.mod_mp mp new_resolver in
-    let resolver_out,new_sig =
-      strengthen_and_subst_struct str subst
-	mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
+    let reso',struc' =
+      strengthen_and_subst_struct struc subst
+	mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
     in
     { mb with
       mod_mp = mp;
-      mod_type = SEBstruct(new_sig);
-      mod_expr = Some (SEBident mb.mod_mp);
+      mod_type = NoFunctor struc';
+      mod_expr = Algebraic (NoFunctor (MEident mb.mod_mp));
       mod_delta =
-        if include_b then resolver_out
-	else add_delta_resolver new_resolver resolver_out }
-  |SEBfunctor(arg_id,argb,body) ->
+        if include_b then reso'
+	else add_delta_resolver new_resolver reso' }
+  |MoreFunctor _ ->
     let subst = map_mp mb.mod_mp mp empty_delta_resolver in
-    subst_module subst
-      (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mb
-  | _ ->
-    anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
-
+    subst_module subst do_delta_dom_codom mb
 
 let subst_modtype_and_resolver mtb mp =
-  let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in
+  let subst = map_mp mtb.typ_mp mp empty_delta_resolver in
   let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in
-  let full_subst = (map_mp mtb.typ_mp mp new_delta) in
-  subst_modtype full_subst
-    (fun resolver subst -> subst_dom_codom_delta_resolver subst resolver) mtb
+  let full_subst = map_mp mtb.typ_mp mp new_delta in
+  subst_modtype full_subst do_delta_dom_codom mtb
+
+(** {6 Cleaning a module expression from bounded parts }
 
-(** {6 Cleaning a bounded module expression } *)
+     For instance:
+       functor(X:T)->struct module M:=X end)
+     becomes:
+       functor(X:T)->struct module M:=<content of T> end)
+*)
 
 let rec is_bounded_expr l = function
-  | SEBident mp -> List.mem mp l
-  | SEBapply (fexpr,mexpr,_) ->
-      is_bounded_expr l mexpr || is_bounded_expr l fexpr
+  | MEident (MPbound mbid) -> MBIset.mem mbid l
+  | MEapply (fexpr,mp) ->
+      is_bounded_expr l (MEident mp) || is_bounded_expr l fexpr
   | _ -> false
 
-let rec clean_struct l = function
-  | (lab,SFBmodule mb) as field -> 
-      let clean_typ = clean_expr l mb.mod_type in 
-      let clean_impl = 
-	begin try
-	  if (is_bounded_expr l (Option.get mb.mod_expr)) then
-	    Some clean_typ
-	  else  Some (clean_expr l (Option.get mb.mod_expr))
-	with
-	    Option.IsNone -> None 
-	end in
-	  if clean_typ==mb.mod_type && clean_impl==mb.mod_expr then
-	    field 
-	  else 
-	    (lab,SFBmodule {mb with 
-			      mod_type=clean_typ;
-			      mod_expr=clean_impl})
-  | field -> field
-      
-and clean_expr l = function
- | SEBfunctor (mbid,sigt,str) as s->
-     let str_clean = clean_expr l str in
-     let sig_clean = clean_expr l sigt.typ_expr in 
-       if  str_clean == str && Int.equal (Pervasives.compare sig_clean sigt.typ_expr) 0 then (** FIXME **)
-	 s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
-  | SEBstruct str as s->
-      let str_clean = List.smartmap (clean_struct l) str in
-      if str_clean == str then s else SEBstruct(str_clean)
-  |  str -> str
-
-let rec collect_mbid l = function
-  | SEBfunctor (mbid,sigt,str) as s->
-      let str_clean = collect_mbid ((MPbound mbid)::l) str in 
-	if  str_clean == str then s else 
-      SEBfunctor (mbid,sigt,str_clean)
-  | SEBstruct str as s->
-      let str_clean = List.smartmap (clean_struct l) str in
-      if str_clean == str then s else SEBstruct(str_clean)
-  |  _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
-       
-       
-let clean_bounded_mod_expr = function
-  | SEBfunctor _ as str -> 
-      let str_clean = collect_mbid [] str in 
-	if  str_clean == str then str else str_clean
-  | str -> str
+let rec clean_module l mb =
+  let impl, typ = mb.mod_expr, mb.mod_type in
+  let typ' = clean_signature l typ in
+  let impl' = match impl with
+    | Algebraic (NoFunctor m) when is_bounded_expr l m -> FullStruct
+    | _ -> implem_smartmap (clean_signature l) (clean_expression l) impl
+  in
+  if typ==typ' && impl==impl' then mb
+  else { mb with mod_type=typ'; mod_expr=impl' }
+
+and clean_modtype l mt =
+  let ty = mt.typ_expr in
+  let ty' = clean_signature l ty in
+  if ty==ty' then mt else { mt with typ_expr=ty' }
+
+and clean_field l field = match field with
+  |(lab,SFBmodule mb) ->
+    let mb' = clean_module l mb in
+    if mb==mb' then field else (lab,SFBmodule mb')
+  |_ -> field
+
+and clean_structure l = List.smartmap (clean_field l)
+
+and clean_signature l =
+  functor_smartmap (clean_modtype l) (clean_structure l)
+
+and clean_expression l =
+  functor_smartmap (clean_modtype l) (fun me -> me)
+
+let rec collect_mbid l sign =  match sign with
+  |MoreFunctor (mbid,ty,m) ->
+    let m' = collect_mbid (MBIset.add mbid l) m in
+    if m==m' then sign else MoreFunctor (mbid,ty,m')
+  |NoFunctor struc ->
+    let struc' = clean_structure l struc in
+    if struc==struc' then sign else NoFunctor struc'
+
+let clean_bounded_mod_expr sign =
+  if is_functor sign then collect_mbid MBIset.empty sign else sign
 
 (** {6 Stm machinery : join and prune } *)
 
-let rec join_module_body mb =
-  Option.iter join_struct_expr_body mb.mod_expr;
-  Option.iter join_struct_expr_body mb.mod_type_alg;
-  join_struct_expr_body mb.mod_type
-and join_structure_body struc =
-  let join_body (l,body) = match body with
-    | SFBconst sb -> join_constant_body sb
-    | SFBmind _ -> ()
-    | SFBmodule m -> join_module_body m
-    | SFBmodtype m ->
-         join_struct_expr_body m.typ_expr;
-         Option.iter join_struct_expr_body m.typ_expr_alg in
-  List.iter join_body struc;
-and join_struct_expr_body = function
-  | SEBfunctor (_,t,e) ->
-      join_struct_expr_body t.typ_expr;
-      Option.iter join_struct_expr_body t.typ_expr_alg;
-      join_struct_expr_body e
-  | SEBident mp -> ()
-  | SEBstruct s -> join_structure_body s
-  | SEBapply (mexpr,marg,u) ->
-       join_struct_expr_body mexpr;
-       join_struct_expr_body marg
-  | SEBwith (seb,wdcl) ->
-       join_struct_expr_body seb;
-       match wdcl with
-       | With_module_body _ -> ()
-       | With_definition_body (_, sb) -> join_constant_body sb
-
-let rec prune_module_body mb =
+let rec join_module mb =
+  implem_iter join_signature join_expression mb.mod_expr;
+  Option.iter join_expression mb.mod_type_alg;
+  join_signature mb.mod_type
+and join_modtype mt =
+  Option.iter join_expression mt.typ_expr_alg;
+  join_signature mt.typ_expr
+and join_field (l,body) = match body with
+  |SFBconst sb -> join_constant_body sb
+  |SFBmind _ -> ()
+  |SFBmodule m -> join_module m
+  |SFBmodtype m -> join_modtype m
+and join_structure struc = List.iter join_field struc
+and join_signature sign = functor_iter join_modtype join_structure sign
+and join_expression me = functor_iter join_modtype (fun _ -> ()) me
+
+let rec prune_module mb =
   let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in
-  let me' = Option.smartmap prune_struct_expr_body me in
-  let mta' = Option.smartmap prune_struct_expr_body mta in
-  let mt' = prune_struct_expr_body mt in
+  let mt' = prune_signature mt in
+  let me' = implem_smartmap prune_signature prune_expression me in
+  let mta' = Option.smartmap prune_expression mta in
   if me' == me && mta' == mta && mt' == mt then mb
   else {mb with mod_expr = me'; mod_type_alg = mta'; mod_type = mt'}
-and prune_structure_body struc =
-  let prune_body (l,body as orig) = match body with
-    | SFBconst sb ->
-        let sb' = prune_constant_body sb in
-        if sb == sb' then orig else (l, SFBconst sb')
-    | SFBmind _ -> orig
-    | SFBmodule m ->
-        let m' = prune_module_body m in
-        if m == m' then orig else (l, SFBmodule m')
-    | SFBmodtype m ->
-        let te, te_alg = m.typ_expr, m.typ_expr_alg in
-        let te' = prune_struct_expr_body te in
-        let te_alg' =
-          Option.smartmap prune_struct_expr_body te_alg in
-        if te' == te && te_alg' == te_alg then orig
-        else (l, SFBmodtype {m with typ_expr = te'; typ_expr_alg = te_alg'})
-  in
-  List.smartmap prune_body struc
-and prune_struct_expr_body orig = match orig with
-  | SEBfunctor (id,t,e) ->
-      let te, ta = t.typ_expr, t.typ_expr_alg in
-      let te' = prune_struct_expr_body te in
-      let ta' = Option.smartmap prune_struct_expr_body ta in
-      let e' = prune_struct_expr_body e in
-      if te' == te && ta' == ta && e' == e then orig
-      else SEBfunctor(id, {t with typ_expr = te'; typ_expr_alg = ta'}, e')
-  | SEBident _ -> orig
-  | SEBstruct s ->
-      let s' = prune_structure_body s in
-      if s' == s then orig else SEBstruct s'
-  | SEBapply (mexpr,marg,u) ->
-      let mexpr' = prune_struct_expr_body mexpr in
-      let marg' = prune_struct_expr_body marg in
-      if mexpr' == mexpr && marg' == marg then orig
-      else SEBapply (mexpr', marg', u)
-  | SEBwith (seb,wdcl) ->
-      let seb' = prune_struct_expr_body seb in
-      let wdcl' = match wdcl with
-        | With_module_body _ -> wdcl
-        | With_definition_body (id, sb) ->
-            let sb' = prune_constant_body sb in
-            if sb' == sb then wdcl else With_definition_body (id, sb') in
-      if seb' == seb && wdcl' == wdcl then orig
-      else SEBwith (seb', wdcl')
+and prune_modtype mt =
+  let te, ta = mt.typ_expr, mt.typ_expr_alg in
+  let te' = prune_signature te in
+  let ta' = Option.smartmap prune_expression ta in
+  if te==te' && ta==ta' then mt else { mt with typ_expr=te'; typ_expr_alg=ta' }
+and prune_field (l,body as orig) = match body with
+  |SFBconst sb ->
+    let sb' = prune_constant_body sb in
+    if sb == sb' then orig else (l, SFBconst sb')
+  |SFBmind _ -> orig
+  |SFBmodule m ->
+    let m' = prune_module m in
+    if m == m' then orig else (l, SFBmodule m')
+  |SFBmodtype m ->
+    let m' = prune_modtype m in
+    if m == m' then orig else (l, SFBmodtype m')
+and prune_structure struc = List.smartmap prune_field struc
+and prune_signature sign = functor_smartmap prune_modtype prune_structure sign
+and prune_expression me = functor_smartmap prune_modtype (fun me -> me) me
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e148f9628..6aed95988 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -16,30 +16,43 @@ open Mod_subst
 
 (** {6 Various operations on modules and module types } *)
 
-val module_body_of_type : module_path -> module_type_body  -> module_body
+(** Functors *)
 
-val module_type_of_module :
-  module_path option -> module_body -> module_type_body
+val is_functor : ('ty,'a) functorize -> bool
 
-val destr_functor :
-  struct_expr_body -> MBId.t * module_type_body * struct_expr_body
+val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize
+
+val destr_nofunctor : ('ty,'a) functorize -> 'a
+
+(** Conversions between [module_body] and [module_type_body] *)
+
+val module_type_of_module : module_body -> module_type_body
+val module_body_of_type : module_path -> module_type_body -> module_body
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
-(** {6 Substitutions } *)
+val implem_smartmap :
+  (module_signature -> module_signature) ->
+  (module_expression -> module_expression) ->
+  (module_implementation -> module_implementation)
 
-val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
+(** {6 Substitutions } *)
 
-val subst_signature : substitution -> structure_body -> structure_body
+val subst_signature : substitution -> module_signature -> module_signature
+val subst_structure : substitution -> structure_body -> structure_body
 
 (** {6 Adding to an environment } *)
 
-val add_signature :
+val add_structure :
   module_path -> structure_body -> delta_resolver -> env -> env
 
 (** adds a module and its components, but not the constraints *)
 val add_module : module_body -> env -> env
 
+
+(** same, for a module type *)
+val add_module_type : module_path -> module_type_body -> env -> env
+
 (** {6 Strengthening } *)
 
 val strengthen : module_type_body -> module_path -> module_type_body
@@ -53,17 +66,22 @@ val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body
 val subst_modtype_and_resolver : module_type_body -> module_path ->
   module_type_body
 
-(** {6 Cleaning a bound module expression } *)
+(** {6 Cleaning a module expression from bounded parts }
 
-val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
+     For instance:
+       functor(X:T)->struct module M:=X end)
+     becomes:
+       functor(X:T)->struct module M:=<content of T> end)
+*)
+
+val clean_bounded_mod_expr : module_signature -> module_signature
 
 (** {6 Stm machinery : join and prune } *)
 
-val join_module_body : module_body -> unit
-val join_structure_body : structure_body -> unit
-val join_struct_expr_body : struct_expr_body -> unit
+val join_module : module_body -> unit
+val join_structure : structure_body -> unit
 
-val prune_structure_body : structure_body -> structure_body
+val prune_structure : structure_body -> structure_body
 
 (** {6 Errors } *)
 
@@ -91,12 +109,12 @@ type module_typing_error =
       Label.t * structure_field_body * signature_mismatch_error
   | LabelAlreadyDeclared of Label.t
   | ApplicationToNotPath of module_struct_entry
-  | NotAFunctor of struct_expr_body
+  | NotAFunctor
+  | IsAFunctor
   | IncompatibleModuleTypes of module_type_body * module_type_body
   | NotEqualModulePaths of module_path * module_path
   | NoSuchLabel of Label.t
   | IncompatibleLabels of Label.t * Label.t
-  | SignatureExpected of struct_expr_body
   | NotAModule of string
   | NotAModuleType of string
   | NotAConstant of Label.t
@@ -121,8 +139,6 @@ val error_incompatible_labels : Label.t -> Label.t -> 'a
 
 val error_no_such_label : Label.t -> 'a
 
-val error_signature_expected : struct_expr_body -> 'a
-
 val error_not_a_module : string -> 'a
 
 val error_not_a_constant : Label.t -> 'a
diff --git a/kernel/names.ml b/kernel/names.ml
index fbd26ca3d..0da8fc5d4 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -234,6 +234,7 @@ struct
 end
 
 module MBImap = Map.Make(MBId)
+module MBIset = Set.Make(MBId)
 
 (** {6 Names of structure elements } *)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 8022cb199..c05e30b9b 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -169,6 +169,7 @@ sig
 
 end
 
+module MBIset : Set.S with type elt = MBId.t
 module MBImap : Map.S with type key = MBId.t
 
 (** {6 The module part of the kernel name } *)
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index acb740cd0..55d348550 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -19,13 +19,11 @@ compiler *)
 
 let rec translate_mod prefix mp env mod_expr acc =
   match mod_expr with
-  | SEBident mp' -> assert false
-  | SEBstruct msb ->
-      let env' = add_signature mp msb empty_delta_resolver env in
-      List.fold_left (translate_field prefix mp env') acc msb
-  | SEBfunctor (mbid,mtb,meb) -> acc
-  | SEBapply (f,x,_) -> assert false
-  | SEBwith _ -> assert false
+  | NoFunctor struc ->
+      let env' = add_structure mp struc empty_delta_resolver env in
+      List.fold_left (translate_field prefix mp env') acc struc
+  | MoreFunctor _ -> acc
+
 and translate_field prefix mp env (code, upds as acc) (l,x) =
   match x with
   | SFBconst cb ->
@@ -41,14 +39,14 @@ and translate_field prefix mp env (code, upds as acc) (l,x) =
 let dump_library mp dp env mod_expr =
   if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
   match mod_expr with
-  | SEBstruct msb ->
-      let env = add_signature mp msb empty_delta_resolver env in
+  | NoFunctor struc ->
+      let env = add_structure mp struc empty_delta_resolver env in
       let prefix = mod_uid_of_dirpath dp ^ "." in
-      let t0 = Sys.time () in 
+      let t0 = Sys.time () in
       clear_global_tbl ();
       clear_symb_tbl ();
       let mlcode, upds =
-        List.fold_left (translate_field prefix mp env) ([],empty_updates) msb
+        List.fold_left (translate_field prefix mp env) ([],empty_updates) struc
       in
       let t1 = Sys.time () in
       let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 7b74b00c5..3f413631c 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -13,7 +13,7 @@ open Nativecode
 (** This file implements separate compilation for libraries in the native
 compiler *)
 
-val dump_library : module_path -> dir_path -> env -> struct_expr_body ->
+val dump_library : module_path -> dir_path -> env -> module_signature ->
   global list * symbol array * code_location_updates
 
 val compile_library :
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c7711b137..5ff619ce1 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,8 +194,8 @@ let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
 
 let join_safe_environment e =
-  Modops.join_structure_body e.revstruct;
-  List.fold_left 
+  Modops.join_structure e.revstruct;
+  List.fold_left
     (fun e fc -> add_constraints (Now (Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
@@ -213,7 +213,7 @@ let prune_env env =
 let prune_safe_environment e =
   { e with
     modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE);
-    revstruct = Modops.prune_structure_body e.revstruct;
+    revstruct = Modops.prune_structure e.revstruct;
     future_cst = [];
     env = prune_env e.env }
 
@@ -433,9 +433,9 @@ let add_mind dir l mie senv =
 
 (** Insertion of module types *)
 
-let add_modtype l mte inl senv =
+let add_modtype l params_mte inl senv =
   let mp = MPdot(senv.modpath, l) in
-  let mtb = Mod_typing.translate_module_type senv.env mp inl mte  in
+  let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte  in
   let senv' = add_field (l,SFBmodtype mtb) MT senv in
   mp, senv'
 
@@ -445,16 +445,19 @@ let full_add_module mb senv =
   let senv = add_constraints (Now mb.mod_constraints) senv in
   { senv with env = Modops.add_module mb senv.env }
 
+let full_add_module_type mp mt senv =
+  let senv = add_constraints (Now mt.typ_constraints) senv in
+  { senv with env = Modops.add_module_type mp mt senv.env }
+
 (** Insertion of modules *)
 
 let add_module l me inl senv =
   let mp = MPdot(senv.modpath, l) in
   let mb = Mod_typing.translate_module senv.env mp inl me in
   let senv' = add_field (l,SFBmodule mb) M senv in
-  let senv'' = match mb.mod_type with
-    | SEBstruct _ ->
-      update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv'
-    | _ -> senv'
+  let senv'' =
+    if Modops.is_functor mb.mod_type then senv'
+    else update_resolver (Mod_subst.add_delta_resolver mb.mod_delta) senv'
   in
   (mp,mb.mod_delta),senv''
 
@@ -489,27 +492,24 @@ let start_modtype l senv =
 let add_module_parameter mbid mte inl senv =
   let () = check_empty_struct senv in
   let mp = MPbound mbid in
-  let mtb = Mod_typing.translate_module_type senv.env mp inl mte in
-  let senv = full_add_module (Modops.module_body_of_type mp mtb) senv in
+  let mtb = Mod_typing.translate_modtype senv.env mp inl ([],mte) in
+  let senv = full_add_module_type mp mtb senv in
   let new_variant = match senv.modvariant with
     | STRUCT (params,oldenv) -> STRUCT ((mbid,mtb) :: params, oldenv)
     | SIG (params,oldenv) -> SIG ((mbid,mtb) :: params, oldenv)
     | _ -> assert false
   in
-  let new_paramresolver = match mtb.typ_expr with
-    | SEBstruct _ ->
-      Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver
-    | _ -> senv.paramresolver
+  let new_paramresolver =
+    if Modops.is_functor mtb.typ_expr then senv.paramresolver
+    else Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver
   in
   mtb.typ_delta,
   { senv with
     modvariant = new_variant;
     paramresolver = new_paramresolver }
 
-let functorize_struct params seb0 =
-  List.fold_left
-    (fun seb (arg_id,arg_b) -> SEBfunctor(arg_id,arg_b,seb))
-    seb0 params
+let functorize params init =
+  List.fold_left (fun e (mbid,mt) -> MoreFunctor(mbid,mt,e)) init params
 
 let propagate_loads senv =
   List.fold_left
@@ -520,36 +520,22 @@ let propagate_loads senv =
 (** Build the module body of the current module, taking in account
     a possible return type (_:T) *)
 
+let functorize_module params mb =
+  let f x = functorize params x in
+  { mb with
+    mod_expr = Modops.implem_smartmap f f mb.mod_expr;
+    mod_type = f mb.mod_type;
+    mod_type_alg = Option.map f mb.mod_type_alg }
+
 let build_module_body params restype senv =
-  let mp = senv.modpath in
-  let mexpr = SEBstruct (List.rev senv.revstruct) in
-  let mexpr' = functorize_struct params mexpr in
-  match restype with
-  | None ->
-    { mod_mp = mp;
-      mod_expr = Some mexpr';
-      mod_type = mexpr';
-      mod_type_alg = None;
-      mod_constraints = senv.univ;
-      mod_delta = senv.modresolver;
-      mod_retroknowledge = senv.local_retroknowledge }
-  | Some (res,inl) ->
-    let res_mtb = Mod_typing.translate_module_type senv.env mp inl res in
-    let auto_mtb = {
-      typ_mp = mp;
-      typ_expr = mexpr;
-      typ_expr_alg = None;
-      typ_constraints = Univ.empty_constraint;
-      typ_delta = Mod_subst.empty_delta_resolver} in
-    let cst = Subtyping.check_subtypes senv.env auto_mtb res_mtb in
-    { mod_mp = mp;
-      mod_expr = Some mexpr';
-      mod_type = functorize_struct params res_mtb.typ_expr;
-      mod_type_alg =
-        Option.map (functorize_struct params) res_mtb.typ_expr_alg;
-      mod_constraints = Univ.union_constraints cst senv.univ;
-      mod_delta = res_mtb.typ_delta;
-      mod_retroknowledge = senv.local_retroknowledge }
+  let struc = NoFunctor (List.rev senv.revstruct) in
+  let restype' = Option.map (fun (ty,inl) -> (([],ty),inl)) restype in
+  let mb =
+    Mod_typing.finalize_module senv.env senv.modpath
+      (struc,None,senv.modresolver,senv.univ) restype'
+  in
+  let mb' = functorize_module params mb in
+  { mb' with mod_retroknowledge = senv.local_retroknowledge }
 
 (** Returning back to the old pre-interactive-module environment,
     with one extra component and some updated fields
@@ -582,10 +568,9 @@ let end_module l restype senv =
   let senv'= propagate_loads {senv with env=newenv} in
   let newenv = Environ.add_constraints mb.mod_constraints senv'.env in
   let newenv = Modops.add_module mb newenv in
-  let newresolver = match mb.mod_type with
-    | SEBstruct _ ->
-      Mod_subst.add_delta_resolver mb.mod_delta oldsenv.modresolver
-    | _ -> oldsenv.modresolver
+  let newresolver =
+    if Modops.is_functor mb.mod_type then oldsenv.modresolver
+    else Mod_subst.add_delta_resolver mb.mod_delta oldsenv.modresolver
   in
   (mp,mbids,mb.mod_delta),
   propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv
@@ -596,14 +581,14 @@ let end_modtype l senv =
   let () = check_current_label l mp in
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
-  let auto_tb = SEBstruct (List.rev senv.revstruct) in
+  let auto_tb = NoFunctor (List.rev senv.revstruct) in
   let newenv = oldsenv.env in
   let newenv = Environ.add_constraints senv.univ newenv in
   let newenv = set_engagement_opt newenv senv.engagement in
   let senv' = propagate_loads {senv with env=newenv} in
   let mtb =
     { typ_mp = mp;
-      typ_expr = functorize_struct params auto_tb;
+      typ_expr = functorize params auto_tb;
       typ_expr_alg = None;
       typ_constraints = senv'.univ;
       typ_delta = senv.modresolver }
@@ -616,22 +601,21 @@ let end_modtype l senv =
 (** {6 Inclusion of module or module type } *)
 
 let add_include me is_module inl senv =
+  let open Mod_typing in
   let mp_sup = senv.modpath in
   let sign,cst,resolver =
     if is_module then
-      let sign,_,resolver,cst =
-	Mod_typing.translate_struct_include_module_entry senv.env mp_sup inl me
-      in
-      sign,cst,resolver
+      let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in
+      sign,cst,reso
     else
-      let mtb = Mod_typing.translate_module_type senv.env mp_sup inl me in
+      let mtb = translate_modtype senv.env mp_sup inl ([],me) in
       mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
   in
   let senv = add_constraints (Now cst) senv in
   (* Include Self support  *)
   let rec compute_sign sign mb resolver senv =
     match sign with
-    | SEBfunctor(mbid,mtb,str) ->
+    | MoreFunctor(mbid,mtb,str) ->
       let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
       let senv = add_constraints (Now cst_sub) senv in
       let mpsup_delta =
@@ -639,21 +623,21 @@ let add_include me is_module inl senv =
       in
       let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in
       let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in
-      compute_sign (Modops.subst_struct_expr subst str) mb resolver senv
+      compute_sign (Modops.subst_signature subst str) mb resolver senv
     | str -> resolver,str,senv
   in
   let resolver,sign,senv =
     let mtb =
       { typ_mp = mp_sup;
-	typ_expr = SEBstruct (List.rev senv.revstruct);
+	typ_expr = NoFunctor (List.rev senv.revstruct);
 	typ_expr_alg = None;
 	typ_constraints = Univ.empty_constraint;
 	typ_delta = senv.modresolver } in
     compute_sign sign mtb resolver senv
   in
   let str = match sign with
-    | SEBstruct str_l -> str_l
-    | _ -> Modops.error_higher_order_include ()
+    | NoFunctor struc -> struc
+    | MoreFunctor _ -> Modops.error_higher_order_include ()
   in
   let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv
   in
@@ -682,7 +666,7 @@ type compiled_library = {
 
 type native_library = Nativecode.global list
 
-let join_compiled_library l = Modops.join_module_body l.comp_mod
+let join_compiled_library l = Modops.join_module l.comp_mod
 
 let start_library dir senv =
   check_initial senv;
@@ -702,10 +686,10 @@ let export senv dir =
   in
   let () = check_current_library dir senv in
   let mp = senv.modpath in
-  let str = SEBstruct (List.rev senv.revstruct) in
+  let str = NoFunctor (List.rev senv.revstruct) in
   let mb =
     { mod_mp = mp;
-      mod_expr = Some str;
+      mod_expr = FullStruct;
       mod_type = str;
       mod_type_alg = None;
       mod_constraints = senv.univ;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 3d67f6c07..5d1c98de5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -73,7 +73,7 @@ val add_module :
   Label.t -> Entries.module_entry -> Declarations.inline ->
     (module_path * Mod_subst.delta_resolver) safe_transformer
 val add_modtype :
-  Label.t -> Entries.module_struct_entry -> Declarations.inline ->
+  Label.t -> Entries.module_type_entry -> Declarations.inline ->
     module_path safe_transformer
 
 (** Adding universe constraints *)
@@ -94,6 +94,8 @@ val add_module_parameter :
   MBId.t -> Entries.module_struct_entry -> Declarations.inline ->
     Mod_subst.delta_resolver safe_transformer
 
+(** The optional result type is given without its functorial part *)
+
 val end_module :
   Label.t -> (Entries.module_struct_entry * Declarations.inline) option ->
     (module_path * MBId.t list * Mod_subst.delta_resolver) safe_transformer
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 99c1b8483..6cedb6ad2 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -319,10 +319,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        check_conv error cst conv env ty1 ty2
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
-  let mty1 = module_type_of_module None msb1 in
-  let mty2 =  module_type_of_module None msb2 in
-  let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in
-    cst
+  let mty1 = module_type_of_module msb1 in
+  let mty2 =  module_type_of_module msb2 in
+  check_modtypes cst env mty1 mty2 subst1 subst2 false
 
 and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= 
   let map1 = make_labmap mp1 sig1 in
@@ -344,67 +343,62 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
 	      | Modtype mtb -> mtb
 	      | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
 	    in
-	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
-	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
-	      check_modtypes cst env mtb1 mtb2 subst1 subst2 true
+	    let env =
+              add_module_type mtb2.typ_mp mtb2
+	        (add_module_type mtb1.typ_mp mtb1 env)
+            in
+	    check_modtypes cst env mtb1 mtb2 subst1 subst2 true
   in
     List.fold_left check_one_body cst sig2
 
-and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = 
-  if mtb1==mtb2 then cst else 
-  let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
-  let rec check_structure cst env str1 str2 equiv subst1 subst2 = 
-	match str1,str2 with
-	  | SEBstruct (list1), 
-	    SEBstruct (list2) -> 
-	      if equiv then
-		let subst2 = 
-		  add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
-		Univ.union_constraints 
-		  (check_signatures cst env
-		     mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
-		  mtb1.typ_delta mtb2.typ_delta) 
-		  (check_signatures cst env 
-		     mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
-		  mtb2.typ_delta  mtb1.typ_delta)
-	      else
-		check_signatures cst env
-		  mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
-		  mtb1.typ_delta  mtb2.typ_delta
-	  | SEBfunctor (arg_id1,arg_t1,body_t1),
-	      SEBfunctor (arg_id2,arg_t2,body_t2) ->
-	      let subst1 = 
-		(join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in
-	      let cst = check_modtypes cst env 
-		arg_t2 arg_t1 subst2 subst1
-		equiv in 
-		(* contravariant *)
-	      let env = add_module 
-		(module_body_of_type (MPbound arg_id2) arg_t2) env 
-	      in
-	      let env = match body_t1 with
-		  SEBstruct str -> 
-		    add_module {mod_mp = mtb1.typ_mp;
-				mod_expr = None;
-				mod_type = subst_struct_expr subst1 body_t1;
-				mod_type_alg= None;
-				mod_constraints=mtb1.typ_constraints;
-				mod_retroknowledge = [];
-				mod_delta = mtb1.typ_delta} env
-		| _ -> env
-	      in
-		check_structure cst env body_t1 body_t2 equiv 
-		  subst1
-		  subst2
-	  | _ , _ -> error_incompatible_modtypes mtb1 mtb2
-      in
-     if mtb1'== mtb2' then cst
-     else check_structure cst env mtb1' mtb2' equiv subst1 subst2
+and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
+  if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then cst
+  else
+    let rec check_structure cst env str1 str2 equiv subst1 subst2 =
+      match str1,str2 with
+      |NoFunctor list1,
+       NoFunctor list2 ->
+	if equiv then
+	  let subst2 = add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
+          let cst1 = check_signatures cst env
+	    mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+	    mtb1.typ_delta mtb2.typ_delta
+          in
+          let cst2 = check_signatures cst env
+	    mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
+	    mtb2.typ_delta  mtb1.typ_delta
+	  in
+	  Univ.union_constraints cst1 cst2
+	else
+	  check_signatures cst env
+	    mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+	    mtb1.typ_delta  mtb2.typ_delta
+      |MoreFunctor (arg_id1,arg_t1,body_t1),
+       MoreFunctor (arg_id2,arg_t2,body_t2) ->
+        let mp2 = MPbound arg_id2 in
+	let subst1 = join (map_mbid arg_id1 mp2 arg_t2.typ_delta) subst1 in
+	let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in
+        (* contravariant *)
+	let env = add_module_type mp2 arg_t2 env in
+	let env =
+          if Modops.is_functor body_t1 then env
+          else add_module
+            {mod_mp = mtb1.typ_mp;
+	     mod_expr = Abstract;
+	     mod_type = subst_signature subst1 body_t1;
+	     mod_type_alg = None;
+	     mod_constraints = mtb1.typ_constraints;
+	     mod_retroknowledge = [];
+	     mod_delta = mtb1.typ_delta} env
+	in
+	check_structure cst env body_t1 body_t2 equiv subst1 subst2
+      | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+    in
+    check_structure cst env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2
 
 let check_subtypes env sup super =
-  let env = add_module 
-		(module_body_of_type sup.typ_mp sup) env in
-  check_modtypes empty_constraint env 
+  let env = add_module_type sup.typ_mp sup env in
+  check_modtypes empty_constraint env
     (strengthen sup sup.typ_mp) super empty_subst
     (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false
 
diff --git a/library/assumptions.ml b/library/assumptions.ml
index 2418f0648..b1f133ac3 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -67,6 +67,23 @@ let rec search_cst_label lab = function
   | (l, SFBconst cb) :: _ when Label.equal l lab -> cb
   | _ :: fields -> search_cst_label lab fields
 
+(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But:
+    a) I don't see currently what should be used instead
+    b) this shouldn't be critical for Print Assumption. At worse some
+       constants will have a canonical name which is non-canonical,
+       leading to failures in [Global.lookup_constant], but our own
+       [lookup_constant] should work.
+*)
+
+let rec fields_of_functor f subs mp0 args = function
+  |NoFunctor a -> f subs mp0 args a
+  |MoreFunctor (mbid,_,e) ->
+    match args with
+    | [] -> assert false (* we should only encounter applied functors *)
+    | mpa :: args ->
+      let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in
+      fields_of_functor f subs mp0 args e
+
 let rec lookup_module_in_impl mp =
   try Global.lookup_module mp
   with Not_found ->
@@ -93,43 +110,29 @@ and fields_of_mp mp =
     if mp_eq inner_mp mp then subs
     else add_mp inner_mp mp mb.mod_delta subs
   in
-  Modops.subst_signature subs fields
+  Modops.subst_structure subs fields
 
-and fields_of_mb subs mb args =
-  let seb = match mb.mod_expr with
-    | None -> mb.mod_type (* cf. Declare Module *)
-    | Some seb -> seb
-  in
-  fields_of_seb subs mb.mod_mp seb args
+and fields_of_mb subs mb args = match mb.mod_expr with
+  |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr
+  |Struct sign -> fields_of_signature subs mb.mod_mp args sign
+  |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type
 
-(* TODO: using [empty_delta_resolver] below in [fields_of_seb]
-   is probably slightly incorrect. But:
-    a) I don't see currently what should be used instead
-    b) this shouldn't be critical for Print Assumption. At worse some
-       constants will have a canonical name which is non-canonical,
-       leading to failures in [Global.lookup_constant], but our own
-       [lookup_constant] should work.
-*)
+(** The Abstract case above corresponds to [Declare Module] *)
 
-and fields_of_seb subs mp0 seb args = match seb with
-  | SEBstruct l ->
-    let () = assert (List.is_empty args) in
-    l, mp0, subs
-  | SEBident mp ->
+and fields_of_signature x =
+  fields_of_functor
+    (fun subs mp0 args struc ->
+      assert (List.is_empty args);
+      (struc, mp0, subs)) x
+
+and fields_of_expr subs mp0 args = function
+  |MEident mp ->
     let mb = lookup_module_in_impl (subst_mp subs mp) in
     fields_of_mb subs mb args
-  | SEBapply (seb1,seb2,_) ->
-    (match seb2 with
-      | SEBident mp2 -> fields_of_seb subs mp0 seb1 (mp2::args)
-      | _ -> assert false) (* only legal application is to module names *)
-  | SEBfunctor (mbid,mtb,seb) ->
-    (match args with
-      | [] -> assert false (* we should only encounter applied functors *)
-      | mpa :: args ->
-	let subs = add_mbid mbid mpa empty_delta_resolver subs in
-	fields_of_seb subs mp0 seb args)
-  | SEBwith _ -> assert false (* should not appear in a mod_expr
-				   or mod_type field *)
+  |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1
+  |MEwith _ -> assert false (* no 'with' in [mod_expr] *)
+
+and fields_of_expression x = fields_of_functor fields_of_expr x
 
 let lookup_constant_in_impl cst fallback =
   try
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 5c0700606..8d332b7df 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -336,15 +336,14 @@ let () = ModSubstObjs.set_missing_handler handle_missing_substobjs
 
 (** Turn a chain of [MSEapply] into the head module_path and the
     list of module_path parameters (deepest param coming first).
-    Currently, right part of [MSEapply] must be [MSEident],
-    and left part must be either [MSEident] or another [MSEapply]. *)
+    The left part of a [MSEapply] must be either [MSEident] or
+    another [MSEapply]. *)
 
 let get_applications mexpr =
   let rec get params = function
-    | MSEident mp -> mp, params
-    | MSEapply (fexpr, MSEident mp) -> get (mp::params) fexpr
-    | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr
-    | _ -> error "Application of a non-functor."
+    | MEident mp -> mp, params
+    | MEapply (fexpr, mp) -> get (mp::params) fexpr
+    | MEwith _ -> error "Non-atomic functor application."
   in get [] mexpr
 
 (** Create the substitution corresponding to some functor applications *)
@@ -357,10 +356,10 @@ let rec compute_subst env mbids sign mp_l inl =
 	let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
 	let mb = Environ.lookup_module mp env in
 	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
-	let resolver = match mb.mod_type with
-          | SEBstruct _ ->
-	    Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta
-          | _ -> empty_delta_resolver (* case of a functor *)
+	let resolver =
+          if Modops.is_functor mb.mod_type then empty_delta_resolver
+          else
+            Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta
 	in
 	mbid_left,join (map_mbid mbid mp resolver) subst
 
@@ -386,25 +385,21 @@ let type_of_mod mp env = function
   |false -> (Environ.lookup_modtype mp env).typ_expr
 
 let rec get_module_path = function
-  |MSEident mp -> mp
-  |MSEfunctor (_,_,me) -> get_module_path me
-  |MSEwith (me,_) -> get_module_path me
-  |MSEapply _ as me -> fst (get_applications me)
+  |MEident mp -> mp
+  |MEwith (me,_) -> get_module_path me
+  |MEapply (me,_) -> get_module_path me
 
 (** Substitutive objects of a module expression (or module type) *)
 
 let rec get_module_sobjs is_mod env inl = function
-  |MSEident mp ->
+  |MEident mp ->
     begin match ModSubstObjs.get mp with
     |(mbids,Objs _) when not (ModPath.is_bound mp) ->
       (mbids,Ref (mp, empty_subst)) (* we create an alias *)
     |sobjs -> sobjs
     end
-  |MSEfunctor (mbid,_,mexpr) ->
-    let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in
-    (mbid::mbids, aobjs)
-  |MSEwith (mty, With_Definition _) -> get_module_sobjs is_mod env inl mty
-  |MSEwith (mty, With_Module (idl,mp1)) ->
+  |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty
+  |MEwith (mty, WithMod (idl,mp1)) ->
     assert (not is_mod);
     let sobjs0 = get_module_sobjs is_mod env inl mty in
     assert (sobjs_no_functor sobjs0);
@@ -413,35 +408,27 @@ let rec get_module_sobjs is_mod env inl = function
     let objs0 = expand_sobjs sobjs0 in
     let objs1 = expand_sobjs (ModSubstObjs.get mp1) in
     ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1))
-  |MSEapply _ as me ->
+  |MEapply _ as me ->
     let mp1, mp_l = get_applications me in
-    let mbids, aobjs = get_module_sobjs is_mod env inl (MSEident mp1) in
+    let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in
     let typ = type_of_mod mp1 env is_mod in
     let mbids_left,subst = compute_subst env mbids typ mp_l inl in
     (mbids_left, subst_aobjs subst aobjs)
 
+let get_functor_sobjs is_mod env inl (params,mexpr) =
+  let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in
+  (List.map fst params @ mbids, aobjs)
+
 
 (** {6 Handling of module parameters} *)
 
 (** For printing modules, [process_module_binding] adds names of
     bound module (and its components) to Nametab. It also loads
-    objects associated to it. It may raise a [Failure] when the
-    bound module hasn't an atomic type. *)
-
-let rec seb2mse = function
-  | SEBident mp -> MSEident mp
-  | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s')
-  | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp))
-  | SEBwith (s,With_definition_body(l,cb)) ->
-      (match cb.const_body with
-	| Def c -> MSEwith(seb2mse s,With_Definition(l,Lazyconstr.force c))
-	| _ -> assert false)
-  | _ -> failwith "seb2mse: received a non-atomic seb"
-
-let process_module_binding mbid seb =
+    objects associated to it. *)
+
+let process_module_binding mbid me =
   let dir = DirPath.make [MBId.to_id mbid] in
   let mp = MPbound mbid in
-  let me = seb2mse seb in
   let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in
   let subst = map_mp (get_module_path me) mp empty_delta_resolver in
   let sobjs = subst_sobjs subst sobjs in
@@ -468,7 +455,7 @@ let intern_arg interp_modast acc (idl,(typ,ann)) =
       let resolver = Global.add_module_parameter mbid mty inl in
       let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in
       do_module false Lib.load_objects 1 dir mp sobjs [];
-      (mbid,(mty,inl))::acc)
+      (mbid,mty,inl)::acc)
     acc idl
 
 (** Process a list of declarations of functor parameters
@@ -504,7 +491,7 @@ let check_subtypes mp sub_mtb_l =
   let mb =
     try Global.lookup_module mp with Not_found -> assert false
   in
-  let mtb = Modops.module_type_of_module None mb in
+  let mtb = Modops.module_type_of_module mb in
   check_sub mtb sub_mtb_l
 
 (** Same for module type [mp] *)
@@ -515,24 +502,21 @@ let check_subtypes_mt mp sub_mtb_l =
   in
   check_sub mtb sub_mtb_l
 
-(** Create a functor entry.
+(** Create a params entry.
     In [args], the youngest module param now comes first. *)
 
-let mk_funct_entry args entry0 =
-  List.fold_left
-    (fun entry (arg_id,(arg_t,_)) ->
-      MSEfunctor (arg_id,arg_t,entry))
-    entry0 args
+let mk_params_entry args =
+  List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args
 
 (** Create a functor type struct.
     In [args], the youngest module param now comes first. *)
 
 let mk_funct_type env args seb0 =
   List.fold_left
-    (fun seb (arg_id,(arg_t,arg_inl)) ->
+    (fun seb (arg_id,arg_t,arg_inl) ->
       let mp = MPbound arg_id in
-      let arg_t = Mod_typing.translate_module_type env mp arg_inl arg_t in
-      SEBfunctor(arg_id,arg_t,seb))
+      let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in
+      MoreFunctor(arg_id,arg_t,seb))
     seb0 args
 
 (** Prepare the module type list for check of subtypes *)
@@ -542,7 +526,7 @@ let build_subtypes interp_modast env mp args mtys =
     (fun (m,ann) ->
        let inl = inl2intopt ann in
        let mte,_ = interp_modast env ModType m in
-       let mtb = Mod_typing.translate_module_type env mp inl mte in
+       let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in
        { mtb with typ_expr = mk_funct_type env args mtb.typ_expr })
     mtys
 
@@ -583,7 +567,8 @@ let start_module interp_modast export id args res fs =
     | Enforce (res,ann) ->
         let inl = inl2intopt ann in
 	let mte,_ = interp_modast env ModType res in
-	let _ = Mod_typing.translate_struct_type_entry env inl mte in
+        (* We check immediately that mte is well-formed *)
+	let _ = Mod_typing.translate_mse env None inl mte in
 	Some (mte,inl), []
     | Check resl ->
 	None, build_subtypes interp_modast env mp arg_entries_r resl
@@ -636,32 +621,31 @@ let declare_module interp_modast id args res mexpr_o fs =
   (* We simulate the beginning of an interactive module,
      then we adds the module parameters to the global env. *)
   let mp = Global.start_module id in
-  let arg_entries_r = intern_args interp_modast args
-  in
+  let arg_entries_r = intern_args interp_modast args in
+  let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
-  let mk_entry k m = mk_funct_entry arg_entries_r (fst (interp_modast env k m))
-  in
   let mty_entry_o, subs, inl_res = match res with
     | Enforce (mty,ann) ->
-        Some (mk_entry ModType mty), [], inl2intopt ann
+        Some (fst (interp_modast env ModType mty)), [], inl2intopt ann
     | Check mtys ->
 	None, build_subtypes interp_modast env mp arg_entries_r mtys,
         default_inline ()
   in
   let mexpr_entry_o, inl_expr = match mexpr_o with
     | None -> None, default_inline ()
-    | Some (mexpr,ann) -> Some (mk_entry Module mexpr), inl2intopt ann
+    | Some (mexpr,ann) ->
+      Some (fst (interp_modast env Module mexpr)), inl2intopt ann
   in
-  let entry =
-    {mod_entry_type = mty_entry_o;
-     mod_entry_expr = mexpr_entry_o }
+  let entry = match mexpr_entry_o, mty_entry_o with
+    | None, None -> assert false (* No body, no type ... *)
+    | None, Some typ -> MType (params, typ)
+    | Some body, otyp -> MExpr (params, body, otyp)
   in
   let sobjs, mp0 = match entry with
-    | {mod_entry_type = Some mte} ->
-      get_module_sobjs false env inl_res mte, get_module_path mte
-    | {mod_entry_expr = Some me} ->
-      get_module_sobjs true env inl_expr me, get_module_path me
-    | _ -> assert false (* No type, no body ... *)
+    | MType (_,mte) | MExpr (_,_,Some mte) ->
+      get_functor_sobjs false env inl_res (params,mte), get_module_path mte
+    | MExpr (_,me,None) ->
+      get_functor_sobjs true env inl_expr (params,me), get_module_path me
   in
   (* Undo the simulated interactive building of the module
      and declare the module as a whole *)
@@ -720,16 +704,13 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs =
   (* We simulate the beginning of an interactive module,
      then we adds the module parameters to the global env. *)
   let mp = Global.start_modtype id in
-  let arg_entries_r = intern_args interp_modast args
-  in
+  let arg_entries_r = intern_args interp_modast args in
+  let params = mk_params_entry arg_entries_r in
   let env = Global.env () in
-  let entry,_ = interp_modast env ModType mty in
-  let entry = mk_funct_entry arg_entries_r entry in
-
+  let entry = params, fst (interp_modast env ModType mty) in
   let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in
-
-  let sobjs = get_module_sobjs false env inl entry in
-  let subst = map_mp (get_module_path entry) mp empty_delta_resolver in
+  let sobjs = get_functor_sobjs false env inl entry in
+  let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
   let sobjs = subst_sobjs subst sobjs in
 
   (* Undo the simulated interactive building of the module type
@@ -767,17 +748,17 @@ let rec include_subst env mp reso mbids sign inline = match mbids with
 let rec decompose_functor mpl typ =
   match mpl, typ with
   | [], _ -> typ
-  | _::mpl, SEBfunctor(_,_,str) -> decompose_functor mpl str
+  | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str
   | _ -> error "Application of a functor with too much arguments."
 
 exception NoIncludeSelf
 
 let type_of_incl env is_mod = function
-  |MSEident mp -> type_of_mod mp env is_mod
-  |MSEapply _ as me ->
+  |MEident mp -> type_of_mod mp env is_mod
+  |MEapply _ as me ->
     let mp0, mp_l = get_applications me in
     decompose_functor mp_l (type_of_mod mp0 env is_mod)
-  |_ -> raise NoIncludeSelf
+  |MEwith _ -> raise NoIncludeSelf
 
 let declare_one_include interp_modast (me_ast,annot) =
   let env = Global.env() in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index f18ed2807..89bcccef3 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -118,4 +118,4 @@ val debug_print_modtab : unit -> Pp.std_ppcmds
     bound module hasn't an atomic type. *)
 
 val process_module_binding :
-  MBId.t -> Declarations.struct_expr_body -> unit
+  MBId.t -> Declarations.module_alg_expr -> unit
diff --git a/library/global.mli b/library/global.mli
index 1bc745bb7..c62f51e16 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -46,7 +46,7 @@ val add_module :
   Id.t -> Entries.module_entry -> Declarations.inline ->
     module_path * Mod_subst.delta_resolver
 val add_modtype :
-  Id.t -> Entries.module_struct_entry -> Declarations.inline -> module_path
+  Id.t -> Entries.module_type_entry -> Declarations.inline -> module_path
 val add_include :
   Entries.module_struct_entry -> bool -> Declarations.inline ->
     Mod_subst.delta_resolver
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index cc302b95d..7fffc960b 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Miniml
 open Term
 open Declarations
 open Names
@@ -14,7 +15,6 @@ open Globnames
 open Pp
 open Errors
 open Util
-open Miniml
 open Table
 open Extraction
 open Modutil
@@ -47,7 +47,7 @@ let toplevel_env () =
         end
     | _ -> None
   in
-  SEBstruct (List.rev (List.map_filter get_reference (Lib.contents ())))
+  List.rev (List.map_filter get_reference (Lib.contents ()))
 
 
 let environment_until dir_opt =
@@ -55,11 +55,11 @@ let environment_until dir_opt =
     | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
     | [] -> []
     | d :: l ->
-	match (Global.lookup_module (MPfile d)).mod_expr with
-	  | Some meb ->
-	      if dir_opt = Some d then [MPfile d, meb]
-	      else (MPfile d, meb) :: (parse l)
-	  | _ -> assert false
+      let meb =
+        Modops.destr_nofunctor (Global.lookup_module (MPfile d)).mod_type
+      in
+      if dir_opt = Some d then [MPfile d, meb]
+      else (MPfile d, meb) :: (parse l)
   in parse (Library.loaded_libraries ())
 
 
@@ -168,113 +168,106 @@ let factor_fix env l cb msb =
     labels, recd, msb''
   end
 
-(** Expanding a [struct_expr_body] into a version without abbreviations
+(** Expanding a [module_alg_expr] into a version without abbreviations
     or functor applications. This is done via a detour to entries
     (hack proposed by Elie)
 *)
 
-let rec seb2mse = function
-  | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s')
-  | SEBident mp -> Entries.MSEident mp
-  | _ -> failwith "seb2mse: received a non-atomic seb"
-
-let expand_seb env mp seb =
-  let seb,_,_,_ =
-    let inl = Some (Flags.get_inline_level()) in
-    Mod_typing.translate_struct_module_entry env mp inl (seb2mse seb)
-  in seb
-
-(** When possible, we use the nicer, shorter, algebraic type structures
-    instead of the expanded ones. *)
-
-let my_type_of_mb mb =
-  let m0 = mb.mod_type in
-  match mb.mod_type_alg with Some m -> m0,m | None -> m0,m0
-
-let my_type_of_mtb mtb =
-  let m0 = mtb.typ_expr in
-  match mtb.typ_expr_alg with Some m -> m0,m | None -> m0,m0
+let expand_mexpr env mp me =
+  let inl = Some (Flags.get_inline_level()) in
+  let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in
+  sign
 
 (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
     To check with Elie. *)
 
-let rec msid_of_seb = function
-  | SEBident mp -> mp
-  | SEBwith (seb,_) -> msid_of_seb seb
+let rec mp_of_mexpr = function
+  | MEident mp -> mp
+  | MEwith (seb,_) -> mp_of_mexpr seb
   | _ -> assert false
 
-let env_for_mtb_with_def env mp seb idl =
-  let sig_b = match seb with
-    | SEBstruct(sig_b) -> sig_b
-    | _ -> assert false
-  in
+let env_for_mtb_with_def env mp me idl =
+  let struc = Modops.destr_nofunctor me in
   let l = Label.of_id (List.hd idl) in
-  let spot = function (l',SFBconst _) -> l = l' | _ -> false in
-  let before = fst (List.split_when spot sig_b) in
-  Modops.add_signature mp before empty_delta_resolver env
+  let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in
+  let before = fst (List.split_when spot struc) in
+  Modops.add_structure mp before empty_delta_resolver env
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to specifications. *)
 
-let rec extract_sfb_spec env mp = function
+let rec extract_structure_spec env mp = function
   | [] -> []
   | (l,SFBconst cb) :: msig ->
       let kn = Constant.make2 mp l in
       let s = extract_constant_spec env kn cb in
-      let specs = extract_sfb_spec env mp msig in
+      let specs = extract_structure_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
       let mind = MutInd.make2 mp l in
       let s = Sind (mind, extract_inductive env mind) in
-      let specs = extract_sfb_spec env mp msig in
+      let specs = extract_structure_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmodule mb) :: msig ->
-      let specs = extract_sfb_spec env mp msig in
-      let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb mb) in
+      let specs = extract_structure_spec env mp msig in
+      let spec = extract_mb_spec env mb.mod_mp mb in
       (l,Smodule spec) :: specs
   | (l,SFBmodtype mtb) :: msig ->
-      let specs = extract_sfb_spec env mp msig in
-      let spec = extract_seb_spec env mtb.typ_mp (my_type_of_mtb mtb) in
+      let specs = extract_structure_spec env mp msig in
+      let spec = extract_mtb_spec env mtb.typ_mp mtb in
       (l,Smodtype spec) :: specs
 
-(* From [struct_expr_body] to specifications *)
+(* From [module_expression] to specifications *)
 
-(* Invariant: the [seb] given to [extract_seb_spec] should either come
+(* Invariant: the [me] given to [extract_mexpr_spec] should either come
    from a [mod_type] or [type_expr] field, or their [_alg] counterparts.
-   This way, any encountered [SEBident] should be a true module type.
+   This way, any encountered [MEident] should be a true module type.
 *)
 
-and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
-  | SEBident mp -> Visit.add_mp_all mp; MTident mp
-  | SEBwith(seb',With_definition_body(idl,cb))->
-      let env' = env_for_mtb_with_def env (msid_of_seb seb') seb idl in
-      let mt = extract_seb_spec env mp1 (seb,seb') in
-      (match extract_with_type env' cb with (* cb peut contenir des kn  *)
+and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
+  | MEident mp -> Visit.add_mp_all mp; MTident mp
+  | MEwith(me',WithDef(idl,c))->
+      let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in
+      let mt = extract_mexpr_spec env mp1 (me_struct,me') in
+      (match extract_with_type env' c with (* cb may contain some kn *)
 	 | None -> mt
 	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
-  | SEBwith(seb',With_module_body(idl,mp))->
+  | MEwith(me',WithMod(idl,mp))->
       Visit.add_mp_all mp;
-      MTwith(extract_seb_spec env mp1 (seb,seb'),
-	     ML_With_module(idl,mp))
-  | SEBfunctor (mbid, mtb, seb_alg') ->
-      let seb' = match seb with
-	| SEBfunctor (mbid',_,seb') when mbid' = mbid -> seb'
+      MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
+  | MEapply _ -> extract_msignature_spec env mp1 me_struct
+
+and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
+  | MoreFunctor (mbid, mtb, me_alg') ->
+      let me_struct' = match me_struct with
+	| MoreFunctor (mbid',_,me') when MBId.equal mbid' mbid -> me'
 	| _ -> assert false
       in
       let mp = MPbound mbid in
-      let env' = Modops.add_module (Modops.module_body_of_type mp mtb) env in
-      MTfunsig (mbid, extract_seb_spec env mp (my_type_of_mtb mtb),
-		extract_seb_spec env' mp1 (seb',seb_alg'))
-  | SEBstruct (msig) ->
-      let env' = Modops.add_signature mp1 msig empty_delta_resolver env in
-      MTsig (mp1, extract_sfb_spec env' mp1 msig)
-  | SEBapply _ ->
-      if seb <> seb_alg then extract_seb_spec env mp1 (seb,seb)
-      else assert false
+      let env' = Modops.add_module_type mp mtb env in
+      MTfunsig (mbid, extract_mtb_spec env mp mtb,
+		extract_mexpression_spec env' mp1 (me_struct',me_alg'))
+  | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m)
+
+and extract_msignature_spec env mp1 = function
+  | NoFunctor struc ->
+      let env' = Modops.add_structure mp1 struc empty_delta_resolver env in
+      MTsig (mp1, extract_structure_spec env' mp1 struc)
+  | MoreFunctor (mbid, mtb, me) ->
+      let mp = MPbound mbid in
+      let env' = Modops.add_module_type mp mtb env in
+      MTfunsig (mbid, extract_mtb_spec env mp mtb,
+		extract_msignature_spec env' mp1 me)
 
+and extract_mtb_spec env mp mtb = match mtb.typ_expr_alg with
+  | Some ty -> extract_mexpression_spec env mp (mtb.typ_expr,ty)
+  | None -> extract_msignature_spec env mp mtb.typ_expr
 
+and extract_mb_spec env mp mb = match mb.mod_type_alg with
+  | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty)
+  | None -> extract_msignature_spec env mp mb.mod_type
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to implementations.
@@ -283,13 +276,13 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
    important: last to first ensures correct dependencies.
 *)
 
-let rec extract_sfb env mp all = function
+let rec extract_structure env mp all = function
   | [] -> []
-  | (l,SFBconst cb) :: msb ->
+  | (l,SFBconst cb) :: struc ->
       (try
-	 let vl,recd,msb = factor_fix env l cb msb in
+	 let vl,recd,struc = factor_fix env l cb struc in
 	 let vc = Array.map (Constant.make2 mp) vl in
-	 let ms = extract_sfb env mp all msb in
+	 let ms = extract_structure env mp all struc in
 	 let b = Array.exists Visit.needed_con vc in
 	 if all || b then
 	   let d = extract_fixpoint env vc recd in
@@ -297,7 +290,7 @@ let rec extract_sfb env mp all = function
 	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms
        with Impossible ->
-	 let ms = extract_sfb env mp all msb in
+	 let ms = extract_structure env mp all struc in
 	 let c = Constant.make2 mp l in
 	 let b = Visit.needed_con c in
 	 if all || b then
@@ -305,8 +298,8 @@ let rec extract_sfb env mp all = function
 	   if (not b) && (logical_decl d) then ms
 	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms)
-  | (l,SFBmind mib) :: msb ->
-      let ms = extract_sfb env mp all msb in
+  | (l,SFBmind mib) :: struc ->
+      let ms = extract_structure env mp all struc in
       let mind = MutInd.make2 mp l in
       let b = Visit.needed_ind mind in
       if all || b then
@@ -314,41 +307,54 @@ let rec extract_sfb env mp all = function
 	if (not b) && (logical_decl d) then ms
 	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
       else ms
-  | (l,SFBmodule mb) :: msb ->
-      let ms = extract_sfb env mp all msb in
+  | (l,SFBmodule mb) :: struc ->
+      let ms = extract_structure env mp all struc in
       let mp = MPdot (mp,l) in
       if all || Visit.needed_mp mp then
 	(l,SEmodule (extract_module env mp true mb)) :: ms
       else ms
-  | (l,SFBmodtype mtb) :: msb ->
-      let ms = extract_sfb env mp all msb in
+  | (l,SFBmodtype mtb) :: struc ->
+      let ms = extract_structure env mp all struc in
       let mp = MPdot (mp,l) in
-       if all || Visit.needed_mp mp then
-	(l,SEmodtype (extract_seb_spec env mp (my_type_of_mtb mtb))) :: ms
+      if all || Visit.needed_mp mp then
+        (l,SEmodtype (extract_mtb_spec env mp mtb)) :: ms
       else ms
 
-(* From [struct_expr_body] to implementations *)
+(* From [module_expr] and [module_expression] to implementations *)
 
-and extract_seb env mp all = function
-  | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml ->
+and extract_mexpr env mp all = function
+  | MEwith _ -> assert false (* no 'with' syntax for modules *)
+  | me when lang () <> Ocaml ->
       (* in Haskell/Scheme, we expand everything *)
-      extract_seb env mp all (expand_seb env mp seb)
-  | SEBident mp ->
+      extract_msignature env mp all (expand_mexpr env mp me)
+  | MEident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
-      Visit.add_mp_all mp; MEident mp
-  | SEBapply (meb, meb',_) ->
-      MEapply (extract_seb env mp true meb,
-	       extract_seb env mp true meb')
-  | SEBfunctor (mbid, mtb, meb) ->
+      Visit.add_mp_all mp; Miniml.MEident mp
+  | MEapply (me, arg) ->
+      Miniml.MEapply (extract_mexpr env mp true me,
+	              extract_mexpr env mp true (MEident arg))
+
+and extract_mexpression env mp all = function
+  | NoFunctor me -> extract_mexpr env mp all me
+  | MoreFunctor (mbid, mtb, me) ->
       let mp1 = MPbound mbid in
-      let env' = Modops.add_module (Modops.module_body_of_type  mp1 mtb)
-	env  in
-      MEfunctor (mbid, extract_seb_spec env mp1 (my_type_of_mtb mtb),
-		 extract_seb env' mp true meb)
-  | SEBstruct (msb) ->
-      let env' = Modops.add_signature mp msb empty_delta_resolver env in
-      MEstruct (mp,extract_sfb env' mp all msb)
-  | SEBwith (_,_) -> anomaly (Pp.str "Not available yet")
+      let env' = Modops.add_module_type mp1 mtb	env in
+      Miniml.MEfunctor
+        (mbid,
+         extract_mtb_spec env mp1 mtb,
+	 extract_mexpression env' mp true me)
+
+and extract_msignature env mp all = function
+  | NoFunctor struc ->
+      let env' = Modops.add_structure mp struc empty_delta_resolver env in
+      Miniml.MEstruct (mp,extract_structure env' mp all struc)
+  | MoreFunctor (mbid, mtb, me) ->
+      let mp1 = MPbound mbid in
+      let env' = Modops.add_module_type mp1 mtb	env in
+      Miniml.MEfunctor
+        (mbid,
+         extract_mtb_spec env mp1 mtb,
+	 extract_msignature env' mp true me)
 
 and extract_module env mp all mb =
   (* A module has an empty [mod_expr] when :
@@ -357,14 +363,14 @@ and extract_module env mp all mb =
      Since we look at modules from outside, we shouldn't have variables.
      But a Declare Module at toplevel seems legal (cf #2525). For the
      moment we don't support this situation. *)
-  match mb.mod_expr with
-    | None -> error_no_module_expr mp
-    | Some me ->
-      { ml_mod_expr = extract_seb env mp all me;
-	ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
-
-
-let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
+  let impl = match mb.mod_expr with
+    | Abstract -> error_no_module_expr mp
+    | Algebraic me -> extract_mexpression env mp all me
+    | Struct sign -> extract_msignature env mp all sign
+    | FullStruct -> extract_msignature env mp all mb.mod_type
+  in
+  { ml_mod_expr = impl;
+    ml_mod_type = extract_mb_spec env mp mb }
 
 let mono_environment refs mpl =
   Visit.reset ();
@@ -373,7 +379,8 @@ let mono_environment refs mpl =
   let env = Global.env () in
   let l = List.rev (environment_until None) in
   List.rev_map
-    (fun (mp,m) -> mp, unpack (extract_seb env mp (Visit.needed_mp_all mp) m))
+    (fun (mp,struc) ->
+      mp, extract_structure env mp (Visit.needed_mp_all mp) struc)
     l
 
 (**************************************)
@@ -620,9 +627,9 @@ let extraction_library is_rec m =
   Visit.add_mp_all (MPfile dir_m);
   let env = Global.env () in
   let l = List.rev (environment_until (Some dir_m)) in
-  let select l (mp,meb) =
+  let select l (mp,struc) =
     if Visit.needed_mp mp
-    then (mp, unpack (extract_seb env mp true meb)) :: l
+    then (mp, extract_structure env mp true struc) :: l
     else l
   in
   let struc = List.fold_left select [] l in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 68f832997..6c1be2d36 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1024,17 +1024,12 @@ let extract_constant_spec env kn cb =
 	let t = snd (record_constant_type env kn (Some typ)) in
 	Sval (r, type_expunge env t)
 
-let extract_with_type env cb =
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+let extract_with_type env c =
+  let typ = type_of env c in
   match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
 	let db = db_from_sign s in
-	let c = match cb.const_body with
-	  | Def body -> Lazyconstr.force body
-	  (* A "with Definition ..." is necessarily transparent *)
-	  | Undef _ | OpaqueDef _ -> assert false
-	in
 	let t = extract_type_scheme env db c (List.length s) in
 	Some (vl, t)
     | _ -> None
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 3a5fc9794..89db50e63 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -19,7 +19,7 @@ val extract_constant : env -> constant -> constant_body -> ml_decl
 
 val extract_constant_spec : env -> constant -> constant_body -> ml_spec
 
-val extract_with_type : env -> constant_body -> ( Id.t list * ml_type ) option
+val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option
 
 val extract_fixpoint :
   env -> constant array -> (constr, types) prec_declaration -> ml_decl
diff --git a/printing/printmod.ml b/printing/printmod.ml
index ee4a2db7f..b5d1d8a18 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -114,18 +114,24 @@ let nametab_register_module_body mp struc =
     nametab_register_dir mp;
     List.iter (nametab_register_body mp DirPath.empty) struc
 
-let nametab_register_module_param mbid seb =
-  (* For algebraic seb, we use a Declaremods function that converts into mse *)
-  try Declaremods.process_module_binding mbid seb
-  with e when Errors.noncritical e ->
-    (* Otherwise, for expanded structure, we try to play with the nametab *)
-    match seb with
-      | SEBstruct struc ->
-        let mp = MPbound mbid in
-        let dir = DirPath.make [MBId.to_id mbid] in
-        nametab_register_dir mp;
-        List.iter (nametab_register_body mp dir) struc
-      | _ -> ()
+let get_typ_expr_alg mtb = match mtb.typ_expr_alg with
+  | Some (NoFunctor me) -> me
+  | _ -> raise Not_found
+
+let nametab_register_modparam mbid mtb =
+  match mtb.typ_expr with
+  | MoreFunctor _ -> () (* functorial param : nothing to register *)
+  | NoFunctor struc ->
+    (* We first try to use the algebraic type expression if any,
+       via a Declaremods function that converts back to module entries *)
+    try
+      Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
+    with e when Errors.noncritical e ->
+      (* Otherwise, we try to play with the nametab ourselves *)
+      let mp = MPbound mbid in
+      let dir = DirPath.make [MBId.to_id mbid] in
+      nametab_register_dir mp;
+      List.iter (nametab_register_body mp dir) struc
 
 let print_body is_impl env mp (l,body) =
   let name = str (Label.to_string l) in
@@ -161,71 +167,71 @@ let print_body is_impl env mp (l,body) =
 let print_struct is_impl env mp struc =
   prlist_with_sep spc (print_body is_impl env mp) struc
 
+let print_structure is_type env mp locals struc =
+  let env' = Option.map
+    (Modops.add_structure mp struc Mod_subst.empty_delta_resolver) env in
+  nametab_register_module_body mp struc;
+  let kwd = if is_type then "Sig" else "Struct" in
+  hv 2 (str kwd ++ spc () ++ print_struct false env' mp struc ++
+	brk (1,-2) ++ str "End")
+
 let rec flatten_app mexpr l = match mexpr with
-  | SEBapply (mexpr, SEBident arg,_) -> flatten_app mexpr (arg::l)
-  | SEBident mp -> mp::l
-  | _ -> assert false
+  | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l)
+  | MEident mp -> mp::l
+  | MEwith _ -> assert false
 
-let rec print_modtype env mp locals mty =
+let rec print_typ_expr env mp locals mty =
   match mty with
-    | SEBident kn -> print_kn locals kn
-    | SEBfunctor (mbid,mtb1,mtb2) ->
-      let mp1 = MPbound mbid in
-      let env' = Option.map
-	  (Modops.add_module (Modops.module_body_of_type mp1 mtb1)) env in
-      let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
-      let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals
-      in
-      nametab_register_module_param mbid seb1;
-      hov 2 (str "Funsig" ++ spc () ++ str "(" ++
-	       pr_id (MBId.to_id mbid) ++ str ":" ++
-	       print_modtype env mp1 locals seb1 ++
-	       str ")" ++ spc() ++ print_modtype env' mp locals' mtb2)
-  | SEBstruct (sign) ->
-      let env' = Option.map
-	(Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
-      nametab_register_module_body mp sign;
-      hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
-	    brk (1,-2) ++ str "End")
-  | SEBapply _ ->
+  | MEident kn -> print_kn locals kn
+  | MEapply _ ->
       let lapp = flatten_app mty [] in
       let fapp = List.hd lapp in
       let mapp = List.tl lapp in
       hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
 		 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
-  | SEBwith(seb,With_definition_body(idl,cb))->
+  | MEwith(me,WithDef(idl,c))->
       let env' = None in (* TODO: build a proper environment if env <> None *)
-      let s = (String.concat "." (List.map Id.to_string idl)) in
-      hov 2 (print_modtype env' mp locals seb ++ spc() ++ str "with" ++ spc() ++
-	       str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
-  | SEBwith(seb,With_module_body(idl,mp))->
-      let s =(String.concat "." (List.map Id.to_string idl)) in
-      hov 2 (print_modtype env mp locals seb ++ spc() ++ str "with" ++ spc() ++
-	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
-
-let rec print_modexpr env mp locals mexpr = match mexpr with
-  | SEBident mp -> print_modpath locals mp
-  | SEBfunctor (mbid,mty,mexpr) ->
-      let mp' = MPbound mbid in
-      let env' = Option.map
-	(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
-      let typ = Option.default mty.typ_expr mty.typ_expr_alg in
+      let s = String.concat "." (List.map Id.to_string idl) in
+      hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
+             ++ str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
+  | MEwith(me,WithMod(idl,mp))->
+      let s = String.concat "." (List.map Id.to_string idl) in
+      hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++
+             str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())
+
+let print_mod_expr env mp locals = function
+  | MEident mp -> print_modpath locals mp
+  | MEapply _ as me ->
+      let lapp = flatten_app me [] in
+      hov 3
+        (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
+  | MEwith _ -> assert false (* No 'with' syntax for modules *)
+
+let rec print_functor fty fatom is_type env mp locals = function
+  |NoFunctor me -> fatom is_type env mp locals me
+  |MoreFunctor (mbid,mtb1,me2) ->
+      nametab_register_modparam mbid mtb1;
+      let mp1 = MPbound mbid in
+      let pr_mtb1 = fty env mp1 locals mtb1 in
+      let env' = Option.map (Modops.add_module_type mp1 mtb1) env in
       let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in
-      nametab_register_module_param mbid typ;
-      hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(MBId.to_id mbid) ++
-	     str ":" ++ print_modtype env mp' locals typ ++
-      str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
-  | SEBstruct struc ->
-      let env' = Option.map
-	(Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
-      nametab_register_module_body mp struc;
-      hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
-	    brk (1,-2) ++ str "End")
-  | SEBapply _ ->
-      let lapp = flatten_app mexpr [] in
-      hov 3 (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
-  | SEBwith (_,_)-> anomaly (Pp.str "Not available yet")
+      let kwd = if is_type then "Funsig" else "Functor" in
+      hov 2
+        (str kwd ++ spc () ++
+	 str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++
+	 spc() ++ print_functor fty fatom is_type env' mp locals' me2)
+
+let rec print_expression x =
+  print_functor
+    print_modtype
+    (function true -> print_typ_expr | false -> print_mod_expr) x
+
+and print_signature x =
+  print_functor print_modtype print_structure x
 
+and print_modtype env mp locals mtb = match mtb.typ_expr_alg with
+  | Some me -> print_expression true env mp locals me
+  | None -> print_signature true env mp locals mtb.typ_expr
 
 let rec printable_body dir =
   let dir = pop_dirpath dir in
@@ -241,23 +247,28 @@ let rec printable_body dir =
 (** Since we might play with nametab above, we should reset to prior
     state after the printing *)
 
-let print_modexpr' env mp mexpr =
+let print_expression' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_modexpr env mp [] e)) mexpr
+    (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me
 
-let print_modtype' env mp mty =
+let print_signature' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_modtype env mp [] e)) mty
+    (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me
 
-let print_module' env mp with_body mb =
+let unsafe_print_module env mp with_body mb =
   let name = print_modpath [] mp in
+  let pr_equals = spc () ++ str ":= " in
   let body = match with_body, mb.mod_expr with
     | false, _
-    | true, None -> mt()
-    | true, Some mexpr ->
-	spc () ++ str ":= " ++ print_modexpr' env mp mexpr
+    | true, Abstract -> mt()
+    | _, Algebraic me -> pr_equals ++ print_expression' false env mp me
+    | _, Struct sign -> pr_equals ++ print_signature' false env mp sign
+    | _, FullStruct -> pr_equals ++ print_signature' false env mp mb.mod_type
   in
-  let modtype = brk (1,1) ++ str": " ++ print_modtype' env mp mb.mod_type
+  let modtype = match mb.mod_expr, mb.mod_type_alg with
+    | FullStruct, _ -> mt ()
+    | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' true env mp ty
+    | _, _ -> brk (1,1) ++ str": " ++ print_signature' true env mp mb.mod_type
   in
   hv 0 (str "Module " ++ name ++ modtype ++ body)
 
@@ -267,9 +278,9 @@ let print_module with_body mp =
   let me = Global.lookup_module mp in
   try
     if !short then raise ShortPrinting;
-    print_module' (Some (Global.env ())) mp with_body me ++ fnl ()
+    unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl ()
   with e when Errors.noncritical e ->
-    print_module' None mp with_body me ++ fnl ()
+    unsafe_print_module None mp with_body me ++ fnl ()
 
 let print_modtype kn =
   let mtb = Global.lookup_modtype kn in
@@ -278,6 +289,6 @@ let print_modtype kn =
     (str "Module Type " ++ name ++ str " =" ++ spc () ++
      (try
 	if !short then raise ShortPrinting;
-	print_modtype' (Some (Global.env ())) kn mtb.typ_expr
+	print_signature' true (Some (Global.env ())) kn mtb.typ_expr
       with e when Errors.noncritical e ->
-	print_modtype' None kn mtb.typ_expr))
+	print_signature' true None kn mtb.typ_expr))
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index c9090f76e..de77ee131 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -671,8 +671,11 @@ let explain_label_already_declared l =
 let explain_application_to_not_path _ =
   str "Application of modules is restricted to paths."
 
-let explain_not_a_functor mtb =
-  str "Application of not a functor."
+let explain_not_a_functor () =
+  str "Application of a non-functor."
+
+let explain_is_a_functor () =
+  str "Illegal use of a functor."
 
 let explain_incompatible_module_types mexpr1 mexpr2 =
   str "Incompatible module types."
@@ -687,9 +690,6 @@ let explain_incompatible_labels l l' =
   str "Opening and closing labels are not the same: " ++
   str (Label.to_string l) ++ str " <> " ++ str (Label.to_string l') ++ str "!"
 
-let explain_signature_expected mtb =
-  str "Signature expected."
-
 let explain_not_a_module s =
   quote (str s) ++ str " is not a module."
 
@@ -719,12 +719,12 @@ let explain_module_error = function
   | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err
   | LabelAlreadyDeclared l -> explain_label_already_declared l
   | ApplicationToNotPath mexpr -> explain_application_to_not_path mexpr
-  | NotAFunctor mtb -> explain_not_a_functor mtb
+  | NotAFunctor -> explain_not_a_functor ()
+  | IsAFunctor -> explain_is_a_functor ()
   | IncompatibleModuleTypes (m1,m2) -> explain_incompatible_module_types m1 m2
   | NotEqualModulePaths (mp1,mp2) -> explain_not_equal_module_paths mp1 mp2
   | NoSuchLabel l -> explain_no_such_label l
   | IncompatibleLabels (l1,l2) -> explain_incompatible_labels l1 l2
-  | SignatureExpected mtb -> explain_signature_expected mtb
   | NotAModule s -> explain_not_a_module s
   | NotAModuleType s -> explain_not_a_module_type s
   | NotAConstant l -> explain_not_a_constant l