From d584d0643e32f2277b1a38ba46fc92993638492b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:07:00 +0100
Subject: unsafe_type_of -> get_type_of in Hipattern.extract_eq_args

---
 tactics/hipattern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 1f68117a76..c5ed02e043 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -453,7 +453,7 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *)
 
 let extract_eq_args env sigma = function
   | MonomorphicLeibnizEq (e1,e2) ->
-      let t = Typing.unsafe_type_of env sigma e1 in (t,e1,e2)
+      let t = Retyping.get_type_of env sigma e1 in (t,e1,e2)
   | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
   | HeterogenousEq (t1,e1,t2,e2) ->
       if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2)
-- 
cgit v1.2.3