From 9b5ceabc9b62cdf9b806bb4abdff73642113e12e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Oct 2018 20:47:46 +0200
Subject: Deprecating Global.type_of_global_in_context.

Removing a few Global.env in the way.
---
 library/global.mli | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'library')

diff --git a/library/global.mli b/library/global.mli
index 0c59330f6e..42a8005a4f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -133,10 +133,7 @@ val constr_of_global_in_context : Environ.env ->
 
 val type_of_global_in_context : Environ.env -> 
   GlobRef.t -> Constr.types * Univ.AUContext.t
-(** Returns the type of the constant in its local universe
-    context. The type should not be used without pushing it's universe
-    context in the environmnent of usage. For non-universe-polymorphic
-    constants, it does not matter. *)
+  [@@ocaml.deprecated "alias of [Typeops.type_of_global]"]
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
 val universes_of_global : GlobRef.t -> Univ.AUContext.t
-- 
cgit v1.2.3