diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-26 15:55:15 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-26 15:55:15 +0100 |
commit | aff038fbbe5ade8d58a895b3d2f6e32267c5184c (patch) | |
tree | 0598bda5a6432894e4fec9ac071cf9ad544d3ee2 /kernel/mod_typing.ml | |
parent | 010775eba60ea89645792b48a0686ff15c4ebcb5 (diff) | |
parent | 6417a9e72feb39b87f0b456186100b11d1c87d5f (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'kernel/mod_typing.ml')
-rw-r--r-- | kernel/mod_typing.ml | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 0f3ea1d0a..d4b381264 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -351,12 +351,20 @@ let translate_module env mp inl = function 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 +let rec translate_mse_inclmod 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.ContextSet.empty |MEapply (fe,arg) -> - let ftrans = translate_mse_incl env mp inl fe in + let ftrans = translate_mse_inclmod env mp inl fe in translate_apply env inl ftrans arg (fun _ _ -> None) - |_ -> Modops.error_higher_order_include () + |MEwith _ -> assert false (* No 'with' syntax for modules *) + +let translate_mse_incl is_mod env mp inl me = + if is_mod then + translate_mse_inclmod env mp inl me + else + let mtb = translate_modtype env mp inl ([],me) in + let sign = clean_bounded_mod_expr mtb.mod_type in + sign,None,mtb.mod_delta,mtb.mod_constraints |