diff options
| author | Pierre-Marie Pédrot | 2020-07-02 16:11:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | 8db43cac35eaa8f2b8c4f8d777dfaafd1f02f27e (patch) | |
| tree | 01f96317416188e3eb9bdfe22d77075724620869 /tactics/class_tactics.ml | |
| parent | 2423629321d46c7facc59b4206bbb773725ec63d (diff) | |
Do not do a round trip with auto hint representation in autoapply.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 5a8522359d..6c1bdca682 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1231,8 +1231,7 @@ let autoapply c i = (Hints.Hint_db.transparent_state hintdb) in let cty = Tacmach.New.pf_get_type_of gl c in let ce = mk_clenv_from gl (c,cty) in - let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in - unify_resolve ~with_evars:true flags h None <*> + Clenv.res_pf ~with_evars:true ~with_classes:false ~flags 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 |