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.

---
 pretyping/pretyping.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'pretyping/pretyping.mli')

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 0f95d27528..2eaa77b822 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -35,7 +35,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
 type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
-  use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
 }
@@ -95,7 +94,7 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
    with candidate and no other conversion problems that the one in
    [pending], however, it can contain more evars than the pending ones. *)
 
-val solve_remaining_evars : inference_flags ->
+val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
   env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map
 
 (** Checking evars and pending conversion problems are all solved,
-- 
cgit v1.2.3