From 478db417e1a3a493870f012495bbc7348581ac17 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 12 Apr 2019 15:23:57 +0200
Subject: Remove `constr_of_global_in_context`

This function seems unused.
---
 kernel/typeops.mli | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index cc1885f42d..c8f3e506e6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -107,14 +107,6 @@ 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