From c1630c9dcdf91dc965b3c375d68e3338fb737531 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 13:32:47 +0200 Subject: Univs: update checker --- 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 8ccf118d3..7f07f8bf8 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