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]. --- engine/univops.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'engine/univops.mli') diff --git a/engine/univops.mli b/engine/univops.mli index 9af568bcb..30fcc4368 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -9,7 +9,8 @@ open Constr open Univ -(** Shrink a universe context to a restricted set of variables *) +(** The universes of monomorphic constants appear. *) +val universes_of_constr : Environ.env -> constr -> LSet.t -val universes_of_constr : constr -> LSet.t +(** Shrink a universe context to a restricted set of variables *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t -- cgit v1.2.3