diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-21 18:56:43 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-12-22 15:05:47 +0100 |
commit | 5122a39888cfc6afd2383d59465324dd67b69f4a (patch) | |
tree | ecfecd5ee4f2d89b6d61ab3638a30dfce6048af2 /kernel/modops.mli | |
parent | 840cefca77a48ad68641539cd26d8d2e8c9dc031 (diff) |
Inclusion of functors with restricted signature is now forbidden (fix #3746)
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
Diffstat (limited to 'kernel/modops.mli')
-rw-r--r-- | kernel/modops.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index a335ad9b4..86aae598c 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -126,13 +126,12 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string + | IncludeRestrictedFunctor of module_path exception ModuleTypingError of module_typing_error val error_existing_label : Label.t -> 'a -val error_application_to_not_path : module_struct_entry -> 'a - val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a @@ -152,3 +151,5 @@ 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_include_restricted_functor : module_path -> 'a |