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.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/uGraph.ml')

diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index bc624ba56d..95d71965df 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -529,6 +529,11 @@ let add_universe vlev strict g =
 let add_universe_unconstrained vlev g =
   fst (add_universe_gen vlev g)
 
+exception UndeclaredLevel of Univ.Level.t
+let check_declared_universes g us =
+  let check l = if not (UMap.mem l g.entries) then raise (UndeclaredLevel l) in
+  Univ.LSet.iter check us
+
 exception Found_explanation of explanation
 
 let get_explanation strict u v g =
-- 
cgit v1.2.3