diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 8733ca8c2..f0cb65c96 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -67,7 +67,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 @@ -113,9 +112,6 @@ let error_generative_module_expected l = let error_no_such_label_sub l l1 = raise (ModuleTypingError (LabelMissing (l,l1))) -let error_higher_order_include () = - raise (ModuleTypingError HigherOrderInclude) - (** {6 Operations on functors } *) let is_functor = function |