From c1630c9dcdf91dc965b3c375d68e3338fb737531 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Thu, 1 Oct 2015 13:32:47 +0200
Subject: Univs: update checker

---
 checker/environ.ml | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

(limited to 'checker/environ.ml')

diff --git a/checker/environ.ml b/checker/environ.ml
index 6dbc44d6b..f8f5c29b7 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -84,13 +84,20 @@ let push_rec_types (lna,typarray,_) env =
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
 
 (* Universe constraints *)
-let add_constraints c env =
-  if c == Univ.Constraint.empty then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+
+let add_constraints c env =
+  if c == Univ.Constraint.empty then env
+  else map_universes (Univ.merge_constraints c) env
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (Univ.merge_context strict ctx) env
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (Univ.merge_context_set strict ctx) env
 
 let check_constraints cst env =
   Univ.check_constraints cst env.env_stratification.env_universes
-- 
cgit v1.2.3