diff options
| author | Gaëtan Gilbert | 2020-02-06 16:13:32 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 5a2600f47b64495a8754be74f3156f915a2497ec (patch) | |
| tree | 5a43ac5a7f7fccdee7062a9bed372d27996c818b | |
| parent | 598558339afec652467c78d0bd6e472df051ef69 (diff) | |
unsafe_type_of -> get_type_of in Class_tactics.autoapply
| -rw-r--r-- | tactics/class_tactics.ml | 5 |
1 files 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 |