From 2e53939f4ce4bc06a5e7b621bc560d3ebeb59110 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Oct 2018 21:08:32 +0200
Subject: Deprecating unused Engine.type_of_global.

---
 engine/univGen.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine')

diff --git a/engine/univGen.mli b/engine/univGen.mli
index 42756701dc..8af5f8fdb0 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -89,3 +89,4 @@ val constr_of_global : GlobRef.t -> constr
     references and computing their instantiated universe context. (side-effect on the
     universe counter, use with care). *)
 val type_of_global : GlobRef.t -> types in_universe_context_set
+[@@ocaml.deprecated "use [Typeops.type_of_global]"]
-- 
cgit v1.2.3