From 5a2600f47b64495a8754be74f3156f915a2497ec Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Feb 2020 16:13:32 +0100
Subject: unsafe_type_of -> get_type_of in Class_tactics.autoapply

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

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f8cb8870ea..ccd88d2c35 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1202,10 +1202,9 @@ let autoapply c i =
   in
   let flags = auto_unif_flags
     (Hints.Hint_db.transparent_state hintdb) in
-  let cty = Tacmach.New.pf_unsafe_type_of gl c in
+  let cty = Tacmach.New.pf_get_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-    unify_e_resolve false flags gl
-                                 ((c,cty,Univ.ContextSet.empty),0,ce) <*>
+    unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
-- 
cgit v1.2.3