diff options
| author | Pierre Letouzey | 2015-10-25 12:14:12 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-10-25 12:14:12 +0100 |
| commit | c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 (patch) | |
| tree | cfabd3b72d81389cf4a7a93cb656534a570ca6ef /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 4 |
1 files changed, 0 insertions, 4 deletions
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 *) |