aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/g_auto.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/g_auto.ml4')
-rw-r--r--ltac/g_auto.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index 82ba63871..03ef3e5c9 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -43,7 +43,7 @@ END
let eval_uconstrs ist cs =
let flags = {
Pretyping.use_typeclasses = false;
- use_unif_heuristics = true;
+ solve_unification_constraints = true;
use_hook = Some Pfedit.solve_by_implicit_tactic;
fail_evar = false;
expand_evars = true