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 /kernel/modops.mli | |
| parent | 010775eba60ea89645792b48a0686ff15c4ebcb5 (diff) | |
| parent | 6417a9e72feb39b87f0b456186100b11d1c87d5f (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index 6fbcd81d03..a335ad9b4a 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 |