From 63883d37318fa54101b3ec4029cb26f0ae8439a3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:39:06 +0100
Subject: unsafe_type_of -> get_type_of in Elim.induction_trailer

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

diff --git a/tactics/elim.ml b/tactics/elim.ml
index c0d533a6f2..379a8d5401 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -133,7 +133,7 @@ let induction_trailer abs_i abs_j bargs =
     (onLastHypId
        (fun id ->
           Proofview.Goal.enter begin fun gl ->
-          let idty = pf_unsafe_type_of gl (mkVar id) in
+          let idty = pf_get_type_of gl (mkVar id) in
           let fvty = global_vars (pf_env gl) (project gl) idty in
           let possible_bring_hyps =
             (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
-- 
cgit v1.2.3