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.
---
 kernel/safe_typing.ml  | 1 -
 kernel/safe_typing.mli | 3 ---
 2 files changed, 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9d302c69fb..b036aa6a67 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -273,7 +273,6 @@ let add_constraints_list cst senv =
   List.fold_left (fun acc c -> add_constraints c acc) senv cst
 
 let push_context_set poly ctx = add_constraints (Now (poly,ctx))
-let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx))
 
 let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 08b97b718e..6e0febaa3f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -128,9 +128,6 @@ val add_modtype :
 val push_context_set :
   bool -> Univ.ContextSet.t -> safe_transformer0
 
-val push_context :
-  bool -> Univ.UContext.t -> safe_transformer0
-
 val add_constraints :
   Univ.Constraint.t -> safe_transformer0
 
-- 
cgit v1.2.3