From 38e1e823cf5329762e97902a6ded54c95a5a5c61 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 17:13:33 +0100
Subject: unsafe_type_of -> get_type_of in Leminv.lemInv

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

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index cf58c9306c..def4af1ae8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -259,7 +259,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac =
 let lemInv id c =
   Proofview.Goal.enter begin fun gls ->
   try
-    let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_unsafe_type_of gls c) in
+    let clause = mk_clenv_from_env (pf_env gls) (project gls) None (c, pf_get_type_of gls c) in
     let clause = clenv_constrain_last_binding (EConstr.mkVar id) clause in
     Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false
   with
-- 
cgit v1.2.3