From 50f5b99e9ffce8d7a54b1a35b899e0645df72632 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:15:53 +0100
Subject: unsafe_type_of -> get_type_of in Contradiction.contradiction_term

---
 tactics/contradiction.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 1f5a6380fd..c7b6998c8c 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -110,8 +110,7 @@ let contradiction_term (c,lbind as cl) =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    let type_of = Tacmach.New.pf_unsafe_type_of gl in
-    let typ = type_of c in
+    let typ = Tacmach.New.pf_get_type_of gl c in
     let _, ccl = splay_prod env sigma typ in
     if is_empty_type env sigma ccl then
       Tacticals.New.tclTHEN
-- 
cgit v1.2.3