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.

---
 plugins/funind/indfun_common.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6fe6888f3d..61fbca23f2 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -342,7 +342,7 @@ let pr_info f_info =
   str "function_constant_type := " ++
   (try
      Printer.pr_lconstr
-       (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
+       (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
-- 
cgit v1.2.3