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

---
 pretyping/typeclasses.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c4418b5a6..d4fa266c0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -400,7 +400,7 @@ let remove_instance i =
   remove_instance_hint i.is_impl
 
 let declare_instance info local glob =
-  let ty = Global.type_of_global_unsafe glob in
+  let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
-- 
cgit v1.2.3