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/extraction/table.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2642aeefa4..dff3548fd8 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -445,9 +445,10 @@ let error_MPfile_as_mod mp b =
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
 let argnames_of_global r =
-  let typ = Global.type_of_global_unsafe r in
+  let env = Global.env () in
+  let typ, _ = Global.type_of_global_in_context env r in
   let rels,_ =
-    decompose_prod (Reduction.whd_all (Global.env ()) typ) in
+    decompose_prod (Reduction.whd_all env typ) in
   List.rev_map fst rels
 
 let msg_of_implicit = function
@@ -878,7 +879,7 @@ let extract_constant_inline inline r ids s =
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
-	let typ = Global.type_of_global_unsafe (ConstRef kn) in
+	let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
 	let typ = Reduction.whd_all env typ in
 	if Reduction.is_arity env typ
 	  then begin
-- 
cgit v1.2.3