From df6b72e348543a289a2ef3f89f32c905add564bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Oct 2018 20:22:59 +0200
Subject: Moving Global.type_of_global_in_context to Typeops.

It is purely functional, so no need for it to be in global now that
GlobRef.t are in the kernel.

Also updated the comments.
---
 kernel/typeops.mli | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 515e22c99b..e83c1b3dc5 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -96,6 +96,16 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
+(** {6 Type of global references. } *)
+
+val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
+(** Returns the type of the global reference, by creating a fresh
+    instance of polymorphic references and computing their
+    instantiated 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. *)
+
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
-- 
cgit v1.2.3