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/modops.mli | 3 --- 1 file changed, 3 deletions(-) (limited to 'kernel/modops.mli') diff --git a/kernel/modops.mli b/kernel/modops.mli index 6fbcd81d0..a335ad9b4 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -126,7 +126,6 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -153,5 +152,3 @@ val error_incorrect_with_constraint : Label.t -> 'a val error_generative_module_expected : Label.t -> 'a val error_no_such_label_sub : Label.t->string->'a - -val error_higher_order_include : unit -> 'a -- cgit v1.2.3