aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--proofs/pfedit.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f9fb0b76d..7622a8776 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