diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 10 |
2 files changed, 12 insertions, 0 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 5d053e4c87..8a52244df2 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -154,6 +154,8 @@ let implicit_tactic = ref None let declare_implicit_tactic tac = implicit_tactic := Some tac +let clear_implicit_tactic () = implicit_tactic := None + let solve_by_implicit_tactic env sigma evk = let evi = Evd.find_undefined sigma evk in match (!implicit_tactic, snd (evar_source evk sigma)) with 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 + + + + + + + |