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