From ad6d5a658806d1c0cf46a39f58113bfbd2ac808d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 19 Oct 2018 15:10:29 +0200
Subject: Remove the implicit tactic feature following #7229.

---
 vernac/lemmas.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 3b041b7065..d537436c6b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -418,8 +418,8 @@ let start_proof_com ?inference_hook kind thms hook =
     let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in
     let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
     let flags = all_and_fail_flags in
-    let flags = { flags with use_hook = inference_hook } in
-    let evd = solve_remaining_evars flags env evd Evd.empty in
+    let hook = inference_hook in
+    let evd = solve_remaining_evars ?hook flags env evd Evd.empty in
     let ids = List.map RelDecl.get_name ctx in
     check_name_freshness (pi1 kind) id;
     (* XXX: The nf_evar is critical !! *)
-- 
cgit v1.2.3