diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-10-25 12:14:12 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-10-25 12:14:12 +0100 |
| commit | c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 (patch) | |
| tree | cfabd3b72d81389cf4a7a93cb656534a570ca6ef /kernel/mod_typing.ml | |
| parent | 1b029b2163386f20179a61f6bdb68e5532f4c306 (diff) | |
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.
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 922652287..eef83ce74 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -359,4 +359,4 @@ let rec translate_mse_incl env mp inl = function |MEapply (fe,arg) -> let ftrans = translate_mse_incl 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 *) |