From 03bf33b94abcedc8952fd791084c8ffebb695402 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 27 Sep 2018 13:49:54 +0200
Subject: Remove {Safe_typing,Global}.push_context

Adding a ucontext to the global environment only makes sense
internally when checking a polymorphic constant.
---
 library/global.ml  | 1 -
 library/global.mli | 1 -
 2 files changed, 2 deletions(-)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 5872126a12..e872d081d6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -86,7 +86,6 @@ let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
 let push_named_def d = globalize0 (Safe_typing.push_named_def d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
-let push_context b c = globalize0 (Safe_typing.push_context b c)
 
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
diff --git a/library/global.mli b/library/global.mli
index 6aeae9fd02..5205968c7b 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -49,7 +49,6 @@ val add_mind :
 (** Extra universe constraints *)
 val add_constraints : Univ.Constraint.t -> unit
 
-val push_context : bool -> Univ.UContext.t -> unit
 val push_context_set : bool -> Univ.ContextSet.t -> unit
 
 (** Non-interactive modules and module types *)
-- 
cgit v1.2.3