diff options
| author | Maxime Dénès | 2017-04-27 17:51:12 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-27 17:51:12 +0200 |
| commit | 30191ecc9a15156aa146c26177fc21c40ce06f99 (patch) | |
| tree | b25a4986afb3007a01c1d57c41777b8eb986b3b8 /proofs | |
| parent | 338f8df5ea59a46b60fcfbe50e122fd6eee0dc52 (diff) | |
| parent | fa27856d2d4ac0f55b99b9406b74301057deb0aa (diff) | |
Merge PR#586: trivial cleanup commits which does not change Coq API
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |