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/safe_typing.ml | |
| 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/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e0a07dcc3..036555309 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -746,7 +746,7 @@ let end_modtype l senv = let add_include me is_module inl senv = let open Mod_typing in let mp_sup = senv.modpath in - let sign,_,resolver,cst = + let sign,(),resolver,cst = translate_mse_incl is_module senv.env mp_sup inl me in let senv = add_constraints (Now (false, cst)) senv in |