Declarations.mli refactoring: module_type_body = module_body

 After this commit, module_type_body is a particular case of module_type.
 For a [module_type_body], the implementation field [mod_expr] is
 supposed to be always [Abstract]. This is verified by coqchk, even
 if this isn't so crucial, since [mod_expr] is never read in the case
 of a module type.

 Concretely, this amounts to the following rewrite on field names
 for module_type_body:
  - typ_expr --> mod_type
  - typ_expr_alg --> mod_type_alg
  - typ_* --> mod_*
 and adding two new fields to mtb:
  - mod_expr (always containing Abstract)
  - mod_retroknowledge (always containing [])

 This refactoring should be completely transparent for the user.

 Pros: code sharing, for instance subst_modtype = subst_module.
 Cons: a runtime invariant (mod_expr = Abstract) which isn't
 enforced by typing. I tried a polymorphic typing of mod_expr,
 to share field names while not having mtb = mb, but the OCaml
 typechecker isn't clever enough with polymorphic mutual fixpoints,
 and reject code sharing (e.g. between subst_modtype and subst_module).
 In the future (with ocaml>=4), some GADT could maybe help here,
 but for now the current solution seems good enough.

8 files changed, 98 insertions, 151 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 4f1672884..2d5468ff1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -251,17 +251,11 @@ and module_body =
     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 =
-  { 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}
+(** A [module_type_body] is just a [module_body] with no
+    implementation ([mod_expr] always [Abstract]) and also
+    an empty [mod_retroknowledge] *)
+
+and module_type_body = module_body
 
 (** Extra invariants :
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 45dfb22d3..6e5491c0b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -436,7 +436,7 @@ let keep_hyps env needed =
 (* Modules *)
 
 let add_modtype mtb env =
-  let mp = mtb.typ_mp in
+  let mp = mtb.mod_mp in
   let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in
   let new_globals = { env.env_globals with env_modtypes = new_modtypes } in
   { env with env_globals = new_globals }
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 7a9b12c43..39dfa9aa3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -43,8 +43,8 @@ let split_struc k m struc =
     | h::tail -> split (h::rev_before) tail
   in split [] struc
 
-let discr_resolver mtb = match mtb.typ_expr with
-  | NoFunctor _ -> mtb.typ_delta
+let discr_resolver mtb = match mtb.mod_type with
+  | NoFunctor _ -> mtb.mod_delta
   | MoreFunctor _ -> empty_delta_resolver
 
 let rec rebuild_mp mp l =
@@ -233,7 +233,7 @@ let rec translate_mse env mpo inl = function
         mb.mod_type, mb.mod_delta
       |None ->
         let mtb = lookup_modtype mp1 env in
-        mtb.typ_expr, mtb.typ_delta
+        mtb.mod_type, mtb.mod_delta
     in
     sign,Some (MEident mp1),reso,Univ.Constraint.empty
   |MEapply (fe,mp1) ->
@@ -259,6 +259,17 @@ let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
   | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
   | _ -> None
 
+let mk_mod mp e ty ty' cst reso =
+  { mod_mp = mp;
+    mod_expr = e;
+    mod_type = ty;
+    mod_type_alg = ty';
+    mod_constraints = cst;
+    mod_delta = reso;
+    mod_retroknowledge = [] }
+
+let mk_modtype mp ty cst reso = mk_mod mp Abstract ty None cst reso
+
 let rec translate_mse_funct env mpo inl mse = function
   |[] ->
     let sign,alg,reso,cst = translate_mse env mpo inl mse in
@@ -269,19 +280,13 @@ let rec translate_mse_funct env mpo inl mse = function
     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
+    MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.mod_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
+  let mtb = mk_modtype (mp_from_mexpr mte) sign cst reso in
   let mtb' = subst_modtype_and_resolver mtb mp in
-  { mtb' with typ_expr_alg = alg }
+  { mtb' with mod_type_alg = alg }
 
 (** [finalize_module] :
     from an already-translated (or interactive) implementation
@@ -290,30 +295,16 @@ and translate_modtype env mp inl (params,mte) =
 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 = [] }
+    mk_mod mp impl sign None cst reso
   |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.Constraint.empty;
-      typ_delta = reso } in
+    let auto_mtb = mk_modtype mp sign Univ.Constraint.empty 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;
+    { res_mtb with
+      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 = [] }
+      mod_constraints = cst +++ cst' }
 
 let translate_module env mp inl = function
   |MType (params,ty) ->
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 21171705d..2e629a3b5 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -12,11 +12,7 @@ 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.
-*)
+(** Main functions for translating module entries *)
 
 val translate_module :
   env -> module_path -> inline -> module_entry -> module_body
@@ -31,7 +27,6 @@ val translate_modtype :
     - 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].
 *)
 
 type 'alg translation =
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 05eac6221..dcf026caf 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -145,20 +145,11 @@ let rec functor_iter fty f0 = function
 (** {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 }
+  { mb with mod_expr = Abstract; mod_type_alg = None }
 
 let module_body_of_type mp mtb =
-  { mod_mp = mp;
-    mod_type = mtb.typ_expr;
-    mod_type_alg = mtb.typ_expr_alg;
-    mod_expr = Abstract;
-    mod_constraints = mtb.typ_constraints;
-    mod_delta = mtb.typ_delta;
-    mod_retroknowledge = [] }
+  assert (mtb.mod_expr == Abstract);
+  { mtb with mod_mp = mp }
 
 let check_modpath_equiv env mp1 mp2 =
   if ModPath.equal mp1 mp2 then ()
@@ -182,7 +173,7 @@ let implem_iter fs fa impl = match impl with
 
 let id_delta x y = x
 
-let rec subst_with_body sub = function
+let subst_with_body sub = function
   |WithMod(id,mp) as orig ->
     let mp' = subst_mp sub mp in
     if mp==mp' then orig else WithMod(id,mp')
@@ -190,26 +181,7 @@ let rec subst_with_body sub = function
     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
-  let mp' = subst_mp sub mp in
-  let sub =
-    if ModPath.equal mp mp' then sub
-    else add_mp mp mp' empty_delta_resolver sub
-  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
-  else
-    { mtb with
-      typ_mp = mp';
-      typ_expr = ty';
-      typ_expr_alg = aty';
-      typ_delta = delta' }
-
-and subst_structure sub do_delta sign =
+let rec subst_structure sub do_delta sign =
   let subst_body ((l,body) as orig) = match body with
     |SFBconst cb ->
       let cb' = subst_const_body sub cb in
@@ -226,11 +198,12 @@ and subst_structure sub do_delta sign =
   in
   List.smartmap subst_body sign
 
-and subst_module sub do_delta mb =
+and subst_body is_mod sub do_delta mb =
   let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in
   let mp' = subst_mp sub mp in
   let sub =
-    if not (is_functor ty) || ModPath.equal mp mp' then sub
+    if ModPath.equal mp mp' then sub
+    else if is_mod && not (is_functor ty) then sub
     else add_mp mp mp' empty_delta_resolver sub
   in
   let ty' = subst_signature sub do_delta ty in
@@ -250,6 +223,10 @@ and subst_module sub do_delta mb =
       mod_type_alg = aty';
       mod_delta = delta' }
 
+and subst_module sub do_delta mb = subst_body true sub do_delta mb
+
+and subst_modtype sub do_delta mtb = subst_body false sub do_delta mtb
+
 and subst_expr sub do_delta seb = match seb with
   |MEident mp ->
     let mp' = subst_mp sub mp in
@@ -397,19 +374,19 @@ and strengthen_sig mp_from struc mp_to reso = match struc with
 
 let strengthen mtb mp =
   (* Has mtb already been strengthened ? *)
-  if mp_in_delta mtb.typ_mp mtb.typ_delta then mtb
-  else match mtb.typ_expr with
+  if mp_in_delta mtb.mod_mp mtb.mod_delta then mtb
+  else match mtb.mod_type with
   |NoFunctor struc ->
-    let reso',struc' = strengthen_sig mtb.typ_mp struc mp mtb.typ_delta in
+    let reso',struc' = strengthen_sig mtb.mod_mp struc mp mtb.mod_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') }
+      mod_type = NoFunctor struc';
+      mod_delta =
+        add_delta_resolver mtb.mod_delta
+	  (add_mp_delta_resolver mtb.mod_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
+  let constants = inline_of_delta inl mtb.mod_delta in
   let rec make_inline delta = function
     | [] -> delta
     | (lev,kn)::r ->
@@ -556,9 +533,9 @@ let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
     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 new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in
-  let full_subst = map_mp mtb.typ_mp mp new_delta in
+  let subst = map_mp mtb.mod_mp mp empty_delta_resolver in
+  let new_delta = subst_dom_codom_delta_resolver subst mtb.mod_delta in
+  let full_subst = map_mp mtb.mod_mp mp new_delta in
   subst_modtype full_subst do_delta_dom_codom mtb
 
 (** {6 Cleaning a module expression from bounded parts }
@@ -585,11 +562,6 @@ let rec clean_module l mb =
   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
@@ -599,10 +571,10 @@ and clean_field l field = match field with
 and clean_structure l = List.smartmap (clean_field l)
 
 and clean_signature l =
-  functor_smartmap (clean_modtype l) (clean_structure l)
+  functor_smartmap (clean_module l) (clean_structure l)
 
 and clean_expression l =
-  functor_smartmap (clean_modtype l) (fun me -> me)
+  functor_smartmap (clean_module l) (fun me -> me)
 
 let rec collect_mbid l sign =  match sign with
   |MoreFunctor (mbid,ty,m) ->
@@ -630,17 +602,13 @@ let join_structure except otab s =
     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 except otab sb
     |SFBmind _ -> ()
-    |SFBmodule m -> join_module m
-    |SFBmodtype m -> join_modtype m
+    |SFBmodule m |SFBmodtype m -> join_module 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 in
+    functor_iter join_module join_structure sign
+  and join_expression me = functor_iter join_module (fun _ -> ()) me in
   join_structure s
 
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index f33e1eaa6..ddd795917 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -47,13 +47,13 @@ and translate_field prefix mp env acc (l,x) =
 	Pp.msg_debug (Pp.str msg));
      translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
-     let mp = mdtyp.typ_mp in
+     let mp = mdtyp.mod_mp in
      (if !Flags.debug then
 	let msg =
 	  Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
 	in
 	Pp.msg_debug (Pp.str msg));
-     translate_mod prefix mp env mdtyp.typ_expr acc
+     translate_mod prefix mp env mdtyp.mod_type acc
 
 let dump_library mp dp env mod_expr =
   if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index af154afd4..27f94972a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -386,7 +386,7 @@ let constraints_of_sfb env sfb =
   match sfb with
   | SFBconst cb -> globalize_constant_universes env cb
   | SFBmind mib -> globalize_mind_universes mib
-  | SFBmodtype mtb -> [Now mtb.typ_constraints]
+  | SFBmodtype mtb -> [Now mtb.mod_constraints]
   | SFBmodule mb -> [Now mb.mod_constraints]
 
 (** A generic function for adding a new field in a same environment.
@@ -396,7 +396,7 @@ type generic_name =
   | C of constant
   | I of mutual_inductive
   | M (** name already known, cf the mod_mp field *)
-  | MT (** name already known, cf the typ_mp field *)
+  | MT (** name already known, cf the mod_mp field *)
 
 let add_field ((l,sfb) as field) gn senv =
   let mlabs,olabs = match sfb with
@@ -494,7 +494,7 @@ let full_add_module mb senv =
   { 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
+  let senv = add_constraints (Now mt.mod_constraints) senv in
   { senv with env = Modops.add_module_type mp mt senv.env }
 
 (** Insertion of modules *)
@@ -548,10 +548,10 @@ let add_module_parameter mbid mte inl senv =
     | _ -> assert false
   in
   let new_paramresolver =
-    if Modops.is_functor mtb.typ_expr then senv.paramresolver
-    else Mod_subst.add_delta_resolver mtb.typ_delta senv.paramresolver
+    if Modops.is_functor mtb.mod_type then senv.paramresolver
+    else Mod_subst.add_delta_resolver mtb.mod_delta senv.paramresolver
   in
-  mtb.typ_delta,
+  mtb.mod_delta,
   { senv with
     modvariant = new_variant;
     paramresolver = new_paramresolver }
@@ -628,24 +628,27 @@ let end_module l restype senv =
   (mp,mbids,mb.mod_delta),
   propagate_senv (l,SFBmodule mb) newenv newresolver senv' oldsenv
 
+let build_mtb mp sign cst delta =
+  { mod_mp = mp;
+    mod_expr = Abstract;
+    mod_type = sign;
+    mod_type_alg = None;
+    mod_constraints = cst;
+    mod_delta = delta;
+    mod_retroknowledge = [] }
+
 let end_modtype l senv =
   let mp = senv.modpath in
   let params, oldsenv = check_sig senv.modvariant in
   let () = check_current_label l mp in
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
-  let auto_tb = NoFunctor (List.rev senv.revstruct) in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
   let newenv = Environ.add_constraints senv.univ newenv in
   let newenv = set_engagement_opt newenv senv.engagement in
   let senv' = {senv with env=newenv} in
-  let mtb =
-    { typ_mp = mp;
-      typ_expr = functorize params auto_tb;
-      typ_expr_alg = None;
-      typ_constraints = senv'.univ;
-      typ_delta = senv.modresolver }
-  in
+  let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
+  let mtb = build_mtb mp auto_tb senv'.univ senv.modresolver in
   let newenv = Environ.add_modtype mtb senv'.env in
   let newresolver = oldsenv.modresolver in
   (mp,mbids),
@@ -662,7 +665,7 @@ let add_include me is_module inl senv =
       sign,cst,reso
     else
       let mtb = translate_modtype senv.env mp_sup inl ([],me) in
-      mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
+      mtb.mod_type,mtb.mod_constraints,mtb.mod_delta
   in
   let senv = add_constraints (Now cst) senv in
   (* Include Self support  *)
@@ -672,7 +675,7 @@ let add_include me is_module inl senv =
       let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
       let senv = add_constraints (Now cst_sub) senv in
       let mpsup_delta =
-	Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta
+	Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
       in
       let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in
       let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in
@@ -680,12 +683,8 @@ let add_include me is_module inl senv =
     | str -> resolver,str,senv
   in
   let resolver,sign,senv =
-    let mtb =
-      { typ_mp = mp_sup;
-	typ_expr = NoFunctor (List.rev senv.revstruct);
-	typ_expr_alg = None;
-	typ_constraints = Univ.Constraint.empty;
-	typ_delta = senv.modresolver } in
+    let struc = NoFunctor (List.rev senv.revstruct) in
+    let mtb = build_mtb mp_sup struc Univ.Constraint.empty senv.modresolver in
     compute_sign sign mtb resolver senv
   in
   let str = match sign with
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 857f577a8..1cf1e8936 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -401,61 +401,61 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
 	      | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
 	    in
 	    let env =
-              add_module_type mtb2.typ_mp mtb2
-	        (add_module_type mtb1.typ_mp mtb1 env)
+              add_module_type mtb2.mod_mp mtb2
+	        (add_module_type mtb1.mod_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 || mtb1.typ_expr == mtb2.typ_expr then cst
+  if mtb1==mtb2 || mtb1.mod_type == mtb2.mod_type 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 subst2 = add_mp mtb2.mod_mp mtb1.mod_mp mtb1.mod_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
+	    mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2
+	    mtb1.mod_delta mtb2.mod_delta
           in
           let cst2 = check_signatures cst env
-	    mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
-	    mtb2.typ_delta  mtb1.typ_delta
+	    mtb2.mod_mp list2 mtb1.mod_mp list1 subst2 subst1
+	    mtb2.mod_delta  mtb1.mod_delta
 	  in
 	  Univ.Constraint.union cst1 cst2
 	else
 	  check_signatures cst env
-	    mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
-	    mtb1.typ_delta  mtb2.typ_delta
+	    mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2
+	    mtb1.mod_delta  mtb2.mod_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 subst1 = join (map_mbid arg_id1 mp2 arg_t2.mod_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_mp = mtb1.mod_mp;
 	     mod_expr = Abstract;
 	     mod_type = subst_signature subst1 body_t1;
 	     mod_type_alg = None;
-	     mod_constraints = mtb1.typ_constraints;
+	     mod_constraints = mtb1.mod_constraints;
 	     mod_retroknowledge = [];
-	     mod_delta = mtb1.typ_delta} env
+	     mod_delta = mtb1.mod_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
+    check_structure cst env mtb1.mod_type mtb2.mod_type equiv subst1 subst2
 
 let check_subtypes env sup super =
-  let env = add_module_type sup.typ_mp sup env in
+  let env = add_module_type sup.mod_mp sup env in
   check_modtypes Univ.Constraint.empty env
-    (strengthen sup sup.typ_mp) super empty_subst
-    (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false
+    (strengthen sup sup.mod_mp) super empty_subst
+    (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false