From f9526a2bcd05174b7adfe56b7375f0306a2a1e6d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Mar 2017 08:38:00 +0100 Subject: Fast path for implicit tactic solving. We make apparent in the API that the implicit tactic is set or not. This was costing a lot in Pretyping for no useful reason, as it is almost always unset and the default implementation was just failing immediately. --- proofs/pfedit.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7458109fa..aad719db4 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 : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr +val solve_by_implicit_tactic : unit -> (env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr) option -- cgit v1.2.3