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 8ccf118d3b..7f07f8bf84 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 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. --- checker/modops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/modops.ml') diff --git a/checker/modops.ml b/checker/modops.ml index 7f07f8bf84..9f43752620 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*