diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index cd8cbe1ee1..ec25459a9f 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -66,6 +66,14 @@ let error_not_a_constant l = let error_with_incorrect l = error ("Incorrect constraint for label \""^(string_of_label l)^"\"") +let error_local_context lo = + match lo with + None -> + error ("The local context is not empty.") + | (Some l) -> + error ("The local context of the component "^ + (string_of_label l)^" is not empty") + let rec scrape_modtype env = function | MTBident kn -> scrape_modtype env (lookup_modtype kn env) | mtb -> mtb |