diff options
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 0001a6c5ed..1d63486ba1 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -259,8 +259,13 @@ and translate_mexpr env mexpr = match mexpr with | Not_path -> error_application_to_not_path mexpr (* place for nondep_supertype *) in + let resolve = Modops.resolver_of_environment farg_id farg_b mp env in MEBapply(feb,meb,cst), - subst_modtype (map_mbid farg_id mp) fbody_b + (* This is the place where the functor formal parameter is + substituted by the given argument to compute the type of the + functor application. *) + subst_modtype + (map_mbid farg_id mp (Some resolve)) fbody_b | MEstruct (msid,structure) -> let structure,signature = translate_entry_list env msid true structure in MEBstruct (msid,structure), |