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.
---
 tactics/hints.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0c10f32c86..2f2d32e887 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -942,7 +942,7 @@ let make_extern pri pat tacast =
 
 let make_mode ref m = 
   let open Term in
-  let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in
+  let ty, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
   let ctx, t = decompose_prod ty in
   let n = List.length ctx in
   let m' = Array.of_list m in
-- 
cgit v1.2.3