From edb2b2535d62b37c324c98b28802c1b1699d4014 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 25 Nov 2017 22:08:01 +0100 Subject: Restrict universe context when declaring constants in obligations. --- test-suite/success/polymorphism.v | 7 +++++++ vernac/obligations.ml | 12 ++++++++---- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index b3f9a4994..d76b30791 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -461,3 +461,10 @@ Section test_letin_subtyping. Qed. End test_letin_subtyping. + +Module ObligationRegression. + (** Test for a regression encountered when fixing obligations for + stronger restriction of universe context. *) + Require Import CMorphisms. + Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _ _}. +End ObligationRegression. diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 17a596c42..570f2e5b3 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -475,13 +475,17 @@ let declare_definition prg = (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in - let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in - let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in + let typ = nf typ in + let body = nf body in + let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in + let uctx = UState.restrict prg.prg_ctx uvars in + let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in + let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in - let ubinders = UState.universe_binders prg.prg_ctx in + let ubinders = UState.universe_binders uctx in DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r)) let rec lam_index n t acc = match Constr.kind t with -- cgit v1.2.3