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

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index c285f907fc..dd0df7d3d6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -268,6 +268,12 @@ val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
 val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
+val push_subgraph : Univ.ContextSet.t -> env -> env
+(** [push_subgraph univs env] adds the universes and constraints in
+   [univs] to [env] as [push_context_set ~strict:false univs env], and
+   also checks that they do not imply new transitive constraints
+   between pre-existing universes in [env]. *)
+
 val set_engagement : engagement -> env -> env
 val set_typing_flags : typing_flags -> env -> env
 
-- 
cgit v1.2.3