diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 744da223a9..390461d5a0 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -67,6 +67,11 @@ let error_not_a_constant l = let error_with_incorrect l = error ("Incorrect constraint for label \""^(string_of_label l)^"\"") +let error_a_generative_module_expected l = + error ("The module " ^ string_of_label l ^ " is not generative. Only " ^ + "component of generative modules can be changed using the \"with\" " ^ + "construct.") + let error_local_context lo = match lo with None -> |