From 1c1eed73491ea84ee58eec703fbeedf9667a06ef Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:40:15 +0100
Subject: unsafe_type_of -> get_type_of in Inv.raw_inversion

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

(limited to 'tactics')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index be0421d42d..2181eb25af 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -464,7 +464,7 @@ let raw_inversion inv_kind id status names =
     let concl = Proofview.Goal.concl gl in
     let c = mkVar id in
     let (ind, t) =
-      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
+      try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c)
       with UserError _ ->
         let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in
         CErrors.user_err  msg
-- 
cgit v1.2.3