diff options
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index b8f1f66a3c..803bdc8398 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -17,7 +17,7 @@ open Declarations open Entries open Mod_subst (*i*) - +exception Circularity of string (* Various operations on modules and module types *) (* recursively unfold MTBdent module types *) @@ -98,5 +98,9 @@ val error_local_context : label option -> 'a val error_circular_with_module : identifier -> 'a +val error_circularity_in_subtyping : string->string->string-> 'a + +val error_no_such_label_sub : label->string->string->'a + val resolver_of_environment : mod_bound_id -> module_type_body -> module_path -> env -> resolver |