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.

---
 plugins/ssr/ssrcommon.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index be8f3603e4..ddfd4c101f 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -242,7 +242,6 @@ let interp_refine ist gl rc =
   let flags = {
     Pretyping.use_typeclasses = true;
     solve_unification_constraints = true;
-    use_hook = None;
     fail_evar = false;
     expand_evars = true }
   in
-- 
cgit v1.2.3