From 5b8b02cd060097c3c980b0498257c30eda1ad207 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 5 Dec 2017 20:22:14 +0100 Subject: Fix #6323: stronger restrict universe context vs abstract. In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c]. --- vernac/obligations.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'vernac/obligations.ml') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 24d664951..4f011e6ad 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -477,7 +477,10 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () 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 env = Global.env () in + let uvars = Univ.LSet.union + (Univops.universes_of_constr env typ) + (Univops.universes_of_constr env 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 -- cgit v1.2.3