From 3d0d56f3f0da9d9b459b6178d2afeaf19fda7d41 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 20:38:20 +0100
Subject: unsafe_type_of -> get_type_of in Coq_omega.destructure_hyps

---
 plugins/omega/coq_omega.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index dcd85401d6..979e5bb8d8 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1713,7 +1713,6 @@ let onClearedName2 id tac =
 
 let destructure_hyps =
   Proofview.Goal.enter begin fun gl ->
-  let type_of = Tacmach.New.pf_unsafe_type_of gl in
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let decidability = decidability env sigma in
@@ -1759,7 +1758,7 @@ let destructure_hyps =
           | Kimp(t1,t2) ->
               (* t1 and t2 might be in Type rather than Prop.
                  For t1, the decidability check will ensure being Prop. *)
-              if Termops.is_Prop sigma (type_of t2)
+              if Termops.is_Prop sigma (Retyping.get_type_of env sigma t2)
               then
                 let d1 = decidability t1 in
                 tclTHENLIST [
-- 
cgit v1.2.3