From 1974816aca996fe3ee9420b83f11d15923e70fda Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 28 Jul 2017 11:41:25 +0200 Subject: Separating the module_type and module_body types by using a type parameter. As explained in edf85b9, the original commit that merged the module_body and module_type_body representations, this was delayed to a later time assumedly due to OCaml lack of GADTs. Actually, the only thing that was needed was polymorphic recursion, which has been around already for a relatively long time (since 3.12). --- kernel/mod_typing.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 0888ccc10..eead5b70d 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) -> @@ -283,7 +285,7 @@ let mk_mod mp e ty cst reso = mod_delta = reso; mod_retroknowledge = [] } -let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso +let mk_modtype mp ty cst reso = mk_mod mp () ty cst reso let rec translate_mse_funct env mpo inl mse = function |[] -> -- cgit v1.2.3