From 8a736c4d3aaf941416ffc616c296a3b077d6242f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 15:48:14 +0100
Subject: unsafe_type_of -> type_of in Tactics.guess_elim

---
 tactics/tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f5685e07af..1624c4a62d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4231,8 +4231,8 @@ let guess_elim isrec dep s hyp0 gl =
         let ind = EConstr.of_constr ind in
         (sigma, ind)
   in
-  let elimt = Typing.unsafe_type_of env sigma elimc in
-    sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
+  let sigma, elimt = Typing.type_of env sigma elimc in
+  sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u)
 
 let given_elim hyp0 (elimc,lbind as e) gl =
   let sigma = Tacmach.New.project gl in
-- 
cgit v1.2.3