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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 8f380830d..a3d502dce 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -924,6 +924,12 @@ let explain_label_missing l s = str "The field " ++ str (Label.to_string l) ++ str " is missing in " ++ str s ++ str "." +let explain_include_restricted_functor mp = + let q = Nametab.shortest_qualid_of_module mp in + str "Cannot include the functor " ++ Libnames.pr_qualid q ++ + strbrk " since it has a restricted signature. " ++ + strbrk "You may name first an instance of this functor, and include it." + let explain_module_error = function | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err | LabelAlreadyDeclared l -> explain_label_already_declared l @@ -940,6 +946,7 @@ let explain_module_error = function | IncorrectWithConstraint l -> explain_incorrect_label_constraint l | GenerativeModuleExpected l -> explain_generative_module_expected l | LabelMissing (l,s) -> explain_label_missing l s + | IncludeRestrictedFunctor mp -> explain_include_restricted_functor mp (* Module internalization errors *) |