diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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. } *) |