diff options
| -rw-r--r-- | tactics/auto.ml | 2 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 2c327b71ba..949db0e0f3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -856,7 +856,7 @@ let delta_full_auto mod_delta n lems gl = let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map (fun x -> searchtable_map x) dbnames in let hyps = pf_hyps gl in - tclTRY (search n false db_list (make_local_hint_db false lems gl) hyps) gl + tclTRY (search n mod_delta db_list (make_local_hint_db false lems gl) hyps) gl let full_auto = delta_full_auto false let new_full_auto = delta_full_auto true diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4319a1d3de..774e03c2cc 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -643,7 +643,7 @@ let rewrite2_unif_flags = { } let convertible env evd x y = - Reductionops.is_trans_conv conv_transparent_state env (Evd.evars_of evd) x y + Reductionops.is_conv env (Evd.evars_of evd) x y let allowK = true |