From cba9f3fe48817e8e524483fd984ea4938b3dc14f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 20 Jul 2017 15:45:17 +0200
Subject: kernel: missing check that all universes are declared.

Keep the universe_levels_of_constr function inside typeops, not
exported.
---
 kernel/uGraph.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/uGraph.mli')

diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8c2d877b0b..752bf76270 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -55,6 +55,12 @@ val add_universe : Level.t -> bool -> t -> t
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
 
+(** Check that the universe levels are declared. Otherwise
+    @raise UndeclaredLevel l for the first undeclared level found. *)
+exception UndeclaredLevel of Univ.Level.t
+
+val check_declared_universes : t -> Univ.LSet.t -> unit
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t
-- 
cgit v1.2.3