From 469a9b3242891b089b4a211e96b5b568277f7fc0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Jul 2017 15:55:51 +0200
Subject: Remove the function Global.type_of_global_unsafe.

---
 API/API.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index f8fb96aa96..e8418552c4 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2713,7 +2713,6 @@ sig
 
   val constr_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
   val type_of_global_in_context : Environ.env -> Globnames.global_reference -> Constr.t * Univ.AUContext.t
-  val type_of_global_unsafe : Globnames.global_reference -> Term.types
 
   val current_dirpath : unit -> Names.DirPath.t
   val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AUContext.t) option
-- 
cgit v1.2.3