From ed04b8eb07ca3925af852c30a75c553c134f7d72 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 29 Oct 2018 17:56:10 +0100
Subject: Local universes for opaque polymorphic constants.

---
 kernel/environ.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 019c0a6819..a6bc579cf7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -380,6 +380,18 @@ let add_universes_set strict ctx g =
 let push_context_set ?(strict=false) ctx env =
   map_universes (add_universes_set strict ctx) env
 
+let push_subgraph (levels,csts) env =
+  let add_subgraph g =
+    let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+    let newg = UGraph.merge_constraints csts newg in
+    (if not (Univ.Constraint.is_empty csts) then
+       let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
+       (if not (UGraph.check_constraints restricted g) then
+          CErrors.anomaly Pp.(str "Local constraints imply new transitive constraints.")));
+    newg
+  in
+  map_universes add_subgraph env
+
 let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
     { env.env_stratification with env_engagement = c } }
-- 
cgit v1.2.3