From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Fri, 13 Nov 2015 11:31:34 +0100
Subject: Imported Upstream version 8.5~beta3+dfsg

---
 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 6fbcd81d..a335ad9b 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