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.
---
 toplevel/himsg.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8efc36df72..8f380830db 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -924,9 +924,6 @@ let explain_label_missing l s =
   str "The field " ++ str (Label.to_string l) ++ str " is missing in "
   ++ str s ++ str "."
 
-let explain_higher_order_include () =
-  str "You cannot Include a higher-order structure."
-
 let explain_module_error = function
   | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err
   | LabelAlreadyDeclared l -> explain_label_already_declared l
@@ -943,7 +940,6 @@ let explain_module_error = function
   | IncorrectWithConstraint l -> explain_incorrect_label_constraint l
   | GenerativeModuleExpected l -> explain_generative_module_expected l
   | LabelMissing (l,s) -> explain_label_missing l s
-  | HigherOrderInclude -> explain_higher_order_include ()
 
 (* Module internalization errors *)
 
-- 
cgit v1.2.3