From 1fd5cec8fbc7323ac7bd710707f37d906c5bc794 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:10:21 +0100
Subject: unsafe_type_of -> get_type_of in Tacticals.general_elim_then_using

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

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ed7ab9164a..5db72e669e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -633,7 +633,7 @@ module New = struct
     (Proofview.Goal.enter begin fun gl ->
     let indclause = mk_clenv_from gl (c, t) in
     (* applying elimination_scheme just a little modified *)
-    let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_unsafe_type_of gl elim)  in
+    let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim)  in
     let indmv =
       match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
-- 
cgit v1.2.3