From 09d0ba708a96125632344f2f994b45e9075fc303 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Oct 2018 20:46:15 +0200
Subject: Moving Global.constr_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.
---
 kernel/typeops.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e83c1b3dc5..1fd070d9d5 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -106,6 +106,14 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
     usage. For non-universe-polymorphic constants, it does not
     matter. *)
 
+(** {6 Building a term from a global reference *)
+
+(** Map a global reference to a term in its local universe
+    context. The term should not be used without pushing it's universe
+    context in the environmnent of usage. For non-universe-polymorphic
+    constants, it does not matter. *)
+val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
+
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
-- 
cgit v1.2.3