diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 0944cbe38f..9ea4027263 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1437,7 +1437,7 @@ let initial_select_evars filter = let resolve_typeclass_evars debug depth unique env evd filter split fail = let evd = - try Evarconv.consider_remaining_unif_problems + try Evarconv.solve_unif_constraints_with_heuristics ~ts:(Typeclasses.classes_transparent_state ()) env evd with e when CErrors.noncritical e -> evd in diff --git a/tactics/equality.ml b/tactics/equality.ml index e9d08d7375..bb3cbad92b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1163,7 +1163,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let dflt_typ = unsafe_type_of env sigma dflt in try let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in - let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in + let () = + evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in dflt with Evarconv.UnableToUnify _ -> error "Cannot solve a unification problem." |