diff options
| author | Pierre-Marie Pédrot | 2015-10-26 15:55:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-26 15:55:15 +0100 |
| commit | aff038fbbe5ade8d58a895b3d2f6e32267c5184c (patch) | |
| tree | 0598bda5a6432894e4fec9ac071cf9ad544d3ee2 /toplevel | |
| parent | 010775eba60ea89645792b48a0686ff15c4ebcb5 (diff) | |
| parent | 6417a9e72feb39b87f0b456186100b11d1c87d5f (diff) | |
Merge branch 'v8.5'
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 *) |