diff options
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 0888ccc10..d2b41aae9 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -264,7 +264,9 @@ let rec translate_mse env mpo inl = function |MEident mp1 as me -> let mb = match mpo with |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false - |None -> lookup_modtype mp1 env + |None -> + let mt = lookup_modtype mp1 env in + module_body_of_type mt.mod_mp mt in mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty |MEapply (fe,mp1) -> @@ -281,9 +283,11 @@ let mk_mod mp e ty cst reso = mod_type_alg = None; mod_constraints = cst; mod_delta = reso; - mod_retroknowledge = [] } + mod_retroknowledge = ModBodyRK []; } -let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso +let mk_modtype mp ty cst reso = + let mb = mk_mod mp Abstract ty cst reso in + { mb with mod_expr = (); mod_retroknowledge = ModTypeRK } let rec translate_mse_funct env mpo inl mse = function |[] -> @@ -319,6 +323,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with { res_mtb with mod_mp = mp; mod_expr = impl; + mod_retroknowledge = ModBodyRK []; (** cst from module body typing, cst' from subtyping, constraints from module type. *) |