diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 813dcaf08..a4c068fa6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1454,8 +1454,14 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = Goal.V82.mk_goal sigma nc gl Store.empty in let gls = { it = gl ; sigma = sigma; } in let hints = searchtable_map typeclasses_db in - let gls' = V85.eauto85 !typeclasses_depth - ~st:(Hint_db.transparent_state hints) [hints] gls in + let st = Hint_db.transparent_state hints in + let depth = get_typeclasses_depth () in + let gls' = + if get_typeclasses_compat () = Flags.Current then + Proofview.V82.of_tactic + (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:false) gls + else V85.eauto85 depth ~st [hints] gls + in let evd = sig_sig gls' in let t' = let (ev, inst) = destEvar t in mkEvar (ev, Array.of_list subst) |