diff options
Diffstat (limited to 'kernel/modops.mli')
| -rw-r--r-- | kernel/modops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index aaff572235..1391380b19 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -92,3 +92,5 @@ val error_not_a_constant : label -> 'a val error_with_incorrect : label -> 'a val error_local_context : label option -> 'a + +val error_circular_with_module : identifier -> 'a |