From 0adf0838a59a3fbca1ced05243ccc42c969fcf18 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 30 Sep 2015 17:49:33 +0200 Subject: Univs: uncovered bug in strengthening of opaque polymorphic definitions. --- kernel/modops.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index d52fe611c0..8733ca8c2f 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -331,8 +331,10 @@ let strengthen_const mp_from l cb resolver = let kn = KerName.make2 mp_from l in let con = constant_of_delta_kn resolver kn in let u = - if cb.const_polymorphic then - Univ.UContext.instance cb.const_universes + if cb.const_polymorphic then + let u = Univ.UContext.instance cb.const_universes in + let s = Univ.make_instance_subst u in + Univ.subst_univs_level_instance s u else Univ.Instance.empty in { cb with -- cgit v1.2.3 From c2de48c3f59415eaf0f2cbb5cfe78f23e908a459 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 25 Oct 2015 12:14:12 +0100 Subject: Minor module cleanup : error HigherOrderInclude was never happening When F is a Functor, doing an 'Include F' triggers the 'Include Self' mechanism: the current context is used as an pseudo-argument to F. This may fail with a subtype error if the current context isn't adequate. --- kernel/modops.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index 8733ca8c2f..f0cb65c967 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -67,7 +67,6 @@ type module_typing_error = | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t | LabelMissing of Label.t * string - | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -113,9 +112,6 @@ let error_generative_module_expected l = let error_no_such_label_sub l l1 = raise (ModuleTypingError (LabelMissing (l,l1))) -let error_higher_order_include () = - raise (ModuleTypingError HigherOrderInclude) - (** {6 Operations on functors } *) let is_functor = function -- cgit v1.2.3 From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Sat, 17 Oct 2015 21:40:49 -0700 Subject: Adds support for the virtual machine to perform reduction of universe polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions. --- kernel/modops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index f0cb65c967..cbb7963315 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -335,7 +335,7 @@ let strengthen_const mp_from l cb resolver = in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) } + const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb -- cgit v1.2.3 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.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index cbb7963315..341c3993a3 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -67,15 +67,13 @@ 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 let error_existing_label l = raise (ModuleTypingError (LabelAlreadyDeclared l)) -let error_application_to_not_path mexpr = - raise (ModuleTypingError (ApplicationToNotPath mexpr)) - let error_not_a_functor () = raise (ModuleTypingError NotAFunctor) @@ -112,6 +110,9 @@ let error_generative_module_expected l = let error_no_such_label_sub l l1 = raise (ModuleTypingError (LabelMissing (l,l1))) +let error_include_restricted_functor mp = + raise (ModuleTypingError (IncludeRestrictedFunctor mp)) + (** {6 Operations on functors } *) let is_functor = function -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/modops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index 341c3993a3..6fe7e382c6 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*