diff options
| author | Maxime Dénès | 2016-11-07 08:42:17 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-07 09:11:47 +0100 |
| commit | 6f30019bfd99a0125fdc12baf8b6c04169701fb7 (patch) | |
| tree | 9fd11119bcf4f4c51baa91de114c246299ddc855 /tactics | |
| parent | 207fcfd9355b01441f2a01614a7de017f4148cde (diff) | |
| parent | e6edb3319c850cc7e30e5c31b0bfbf16c5c1a32c (diff) | |
Merge commit 'e6edb33' into v8.6
Was PR#331: Solve_constraints and Set Use Unification Heuristics
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 4 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 51bf69e5ce..af1ab4197c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1440,7 +1440,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." diff --git a/tactics/tactics.ml b/tactics/tactics.ml index af52c52370..db19d54bd0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1141,7 +1141,7 @@ let run_delayed env sigma c = let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; - Pretyping.use_unif_heuristics = true; + Pretyping.solve_unification_constraints = true; Pretyping.use_hook = Some solve_by_implicit_tactic; Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } |