From c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 25 Oct 2015 12:14:12 +0100 Subject: Minor module cleanup : error HigherOrderInclude was never happening When F is a Functor, doing an 'Include F' triggers the 'Include Self' mechanism: the current context is used as an pseudo-argument to F. This may fail with a subtype error if the current context isn't adequate. --- kernel/mod_typing.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/mod_typing.mli') diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 80db12b0d..0c3fb2ba7 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -36,6 +36,9 @@ val translate_mse : env -> module_path option -> inline -> module_struct_entry -> module_alg_expr translation +(** [translate_mse_incl] translate the mse of a real module (no + module type here) given to an Include *) + val translate_mse_incl : env -> module_path -> inline -> module_struct_entry -> module_alg_expr translation -- cgit v1.2.3