From 598558339afec652467c78d0bd6e472df051ef69 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:11:41 +0100
Subject: unsafe_type_of -> get_type_of in Tacticals.elimination_then

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

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5db72e669e..199fdd50c4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -741,7 +741,7 @@ module New = struct
 
   let elimination_then tac c =
     Proofview.Goal.enter begin fun gl ->
-    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
+    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
       | NotRecord -> true,gl_make_elim
-- 
cgit v1.2.3