From 86c6649382bb9e42281ffe956c627c6d3987559b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 30 May 2014 21:55:24 +0200
Subject: - Force every universe level to be >= Prop, so one cannot "go under"
 it anymore. - Finish the change to level-to-level substitutions, in the
 checker.

---
 kernel/univ.ml  | 6 ++++++
 kernel/univ.mli | 2 ++
 2 files changed, 8 insertions(+)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 147efe86bc..6c60950211 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1466,6 +1466,12 @@ let initial_universes = enforce_univ_lt Level.prop Level.set LMap.empty
 
 let is_initial_universes g = LMap.equal (==) g initial_universes
 
+let add_universe vlev g = 
+  let v = terminal vlev in
+  let proparc = prop_arc g in
+    enter_arc {proparc with le=vlev::proparc.le}
+      (enter_arc v g)
+      
 (* Constraints and sets of constraints. *)    
 
 type univ_constraint = Level.t * constraint_type * Level.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index bf04c62e21..9398e23ba9 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -183,6 +183,8 @@ val initial_universes : universes
 
 val is_initial_universes : universes -> bool
 
+val add_universe : universe_level -> universes -> universes
+
 (** {6 Substitution} *)
 
 type universe_subst_fn = universe_level -> universe
-- 
cgit v1.2.3