From 9b5ceabc9b62cdf9b806bb4abdff73642113e12e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Oct 2018 20:47:46 +0200
Subject: Deprecating Global.type_of_global_in_context.

Removing a few Global.env in the way.
---
 plugins/extraction/table.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction/table.ml')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 7b4fd280bd..f6eea3c5c4 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -446,7 +446,7 @@ let error_MPfile_as_mod mp b =
 
 let argnames_of_global r =
   let env = Global.env () in
-  let typ, _ = Global.type_of_global_in_context env r in
+  let typ, _ = Typeops.type_of_global_in_context env r in
   let rels,_ =
     decompose_prod (Reduction.whd_all env typ) in
   List.rev_map fst rels
@@ -878,7 +878,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_in_context env (ConstRef kn) in
+        let typ, _ = Typeops.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