From 5122a39888cfc6afd2383d59465324dd67b69f4a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 21 Dec 2015 18:56:43 +0100 Subject: 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. --- kernel/modops.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'kernel/modops.mli') 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 -- cgit v1.2.3