aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/univ.mli')
-rw-r--r--kernel/univ.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli
index f139a8b33..114193329 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -462,3 +462,6 @@ val eq_levels : universe_level -> universe_level -> bool
(** deprecated: Equality of formal universe expressions. *)
val equal_universes : universe -> universe -> bool
+
+(** Universes of constraints *)
+val universes_of_constraints : constraints -> universe_set