From fa27856d2d4ac0f55b99b9406b74301057deb0aa Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Thu, 27 Apr 2017 09:57:09 +0200
Subject: contracting the type of "Pfedit.solve_by_implicit_tactic"

---
 proofs/pfedit.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f9fb0b76de..7622a87768 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr) option
+val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
-- 
cgit v1.2.3