aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 18:01:48 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 18:21:25 +0100
commit3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (patch)
tree45fdbfc2fd03e30105d1ead1e184bdf6ef822de8 /pretyping/pretyping.ml
parentcca57bcd89770e76e1bcc21eb41756dca2c51425 (diff)
parent4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff)
Merge branch 'master'.
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 563769df5..846d8055a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -249,7 +249,7 @@ type inference_hook = env -> evar_map -> evar -> evar_map * constr
type inference_flags = {
use_typeclasses : bool;
- use_unif_heuristics : bool;
+ solve_unification_constraints : bool;
use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
@@ -296,7 +296,7 @@ let apply_inference_hook hook evdref pending =
let apply_heuristics env evdref fail_evar =
(* Resolve eagerly, potentially making wrong choices *)
- try evdref := consider_remaining_unif_problems
+ try evdref := solve_unif_constraints_with_heuristics
~ts:(Typeclasses.classes_transparent_state ()) env !evdref
with e when CErrors.noncritical e ->
let e = CErrors.push e in if fail_evar then iraise e
@@ -343,7 +343,7 @@ let solve_remaining_evars flags env current_sigma pending =
if flags.use_typeclasses then apply_typeclasses env evdref frozen false;
if Option.has_some flags.use_hook then
apply_inference_hook (Option.get flags.use_hook env) evdref pending;
- if flags.use_unif_heuristics then apply_heuristics env evdref false;
+ if flags.solve_unification_constraints then apply_heuristics env evdref false;
if flags.fail_evar then check_evars_are_solved env !evdref frozen pending;
!evdref
@@ -1121,14 +1121,14 @@ let ise_pretype_gen flags env sigma lvar kind c =
let default_inference_flags fail = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = fail;
expand_evars = true }
let no_classes_no_fail_inference_flags = {
use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = false;
expand_evars = true }
@@ -1194,7 +1194,7 @@ let understand_ltac flags env sigma lvar kind c =
let constr_flags = {
use_typeclasses = true;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = None;
fail_evar = true;
expand_evars = true }