From 4838a3a3c25cc9f7583dd62e4585460aca8ee961 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 21 Sep 2015 11:55:32 +0200 Subject: Forcing i > Set for global universes (incomplete) --- kernel/univ.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/univ.mli') diff --git a/kernel/univ.mli b/kernel/univ.mli index 76453cbb0..fe7fc1ab9 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -163,8 +163,8 @@ val is_initial_universes : universes -> bool val sort_universes : universes -> universes -(** Adds a universe to the graph, ensuring it is >= Prop or Set. *) -val add_universe : universe_level -> predicative:bool -> universes -> universes +(** Adds a universe to the graph, ensuring it is >= or > Set. *) +val add_universe : universe_level -> bool -> universes -> universes (** {6 Constraints. } *) -- cgit v1.2.3