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

---
 library/global.mli | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/library/global.mli b/library/global.mli
index 29255a70ff..0c59330f6e 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -129,10 +129,7 @@ val is_type_in_type : GlobRef.t -> bool
 
 val constr_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.constr_of_global_in_context]"]
 
 val type_of_global_in_context : Environ.env -> 
   GlobRef.t -> Constr.types * Univ.AUContext.t
-- 
cgit v1.2.3