From 3faf22b382379f08d5a918bd535287f57e2fc0fc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 15:39:49 +0100
Subject: unsafe_type_of -> get_type_of in Tactics.atomize_param_of_ind_then

Not 100% sure about this one TBH, this function is messy.
---
 tactics/tactics.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 87389f0be0..da798dd2ce 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3399,8 +3399,9 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
             let id = match EConstr.kind sigma c with
             | Var id -> id
             | _ ->
-            let type_of = Tacmach.New.pf_unsafe_type_of gl in
-            id_of_name_using_hdchar env sigma (type_of c) Anonymous in
+              let type_of = Tacmach.New.pf_get_type_of gl in
+              id_of_name_using_hdchar env sigma (type_of c) Anonymous
+            in
             let x = fresh_id_in_env avoid id env in
             Tacticals.New.tclTHEN
               (letin_tac None (Name x) c None allHypsAndConcl)
-- 
cgit v1.2.3