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]. --- API/API.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 6227f17c6..b79be8f7d 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2057,7 +2057,7 @@ end module Univops : sig - val universes_of_constr : Constr.constr -> Univ.LSet.t + val universes_of_constr : Environ.env -> Constr.constr -> Univ.LSet.t val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t end -- cgit v1.2.3