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 --- checker/modops.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'checker/modops.ml') diff --git a/checker/modops.ml b/checker/modops.ml index 8ccf118d..7f07f8bf 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -83,12 +83,13 @@ let strengthen_const mp_from l cb resolver = | Def _ -> cb | _ -> let con = Constant.make2 mp_from l in - (* let con = constant_of_delta resolver con in*) let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + if cb.const_polymorphic then + Univ.make_abstract_instance cb.const_universes else Univ.Instance.empty in - { cb with const_body = Def (Declarations.from_val (Const (con,u))) } + { cb with + const_body = Def (Declarations.from_val (Const (con,u))) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb -- cgit v1.2.3