From 5251ffebaa19fa22866ccd537b8d7cfe6aaadf5c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 15:58:43 +0100
Subject: unsafe_type_of -> type_of in Tactics.induction_gen_l + fix bad env

---
 tactics/tactics.ml | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6ed6e49b7e..8f7fbe7552 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4667,18 +4667,16 @@ let induction_gen_l isrec with_evars elim names lc =
 
             | _ ->
                 Proofview.Goal.enter begin fun gl ->
-                let type_of = Tacmach.New.pf_unsafe_type_of gl in
-                let sigma = Tacmach.New.project gl in
-                Proofview.tclENV >>= fun env ->
-                let x =
-                  id_of_name_using_hdchar env sigma (type_of c) Anonymous in
-
+                let sigma, t = pf_apply Typing.type_of gl c in
+                let x = id_of_name_using_hdchar (Proofview.Goal.env gl) sigma t Anonymous in
                 let id = new_fresh_id Id.Set.empty x gl in
                 let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
                 let () = newlc:=id::!newlc in
-                Tacticals.New.tclTHEN
-                  (letin_tac None (Name id) c None allHypsAndConcl)
-                  (atomize_list newl')
+                Tacticals.New.tclTHENLIST [
+                  tclEVARS sigma;
+                  letin_tac None (Name id) c None allHypsAndConcl;
+                  atomize_list newl';
+                ]
                 end in
   Tacticals.New.tclTHENLIST
     [
-- 
cgit v1.2.3