diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index f7c7b36537..6dad738afb 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -166,5 +166,15 @@ val build_by_tactic : env -> types -> unit Proofview.tactic -> constr * bool val declare_implicit_tactic : unit Proofview.tactic -> unit +(** To remove the default tactic *) +val clear_implicit_tactic : unit -> unit + (* Raise Exit if cannot solve *) val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr + + + + + + + |