From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/modops.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) (limited to 'kernel/modops.ml') diff --git a/kernel/modops.ml b/kernel/modops.ml index d52fe611..cbb79633 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 @@ -331,13 +327,15 @@ 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 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