diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:41:46 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:41:46 +0000 |
| commit | 0b936be00d2c7c05d528b8d7304fc1e14d5546a5 (patch) | |
| tree | 01f36ced9e882355658600dc00787043f40ce9e8 /proofs/pfedit.mli | |
| parent | 7a7c00fdc81b450a5b2cb91b64bb2602d24212c1 (diff) | |
Doc: solve the bad interaction between Declare Implicit Tactic and refine.
An implicit tactic was declared and made refine fail (trying to solve the open goals of the refined term resulted in an error). There was no way to remove the implicit tactic (it isn't managed by an option so isn't removed by Reset Initial). I added the option under the name Clear Implicit Tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17032 85f007b7-540e-0410-9357-904b9bb8a0f7
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 f7c7b3653..6dad738af 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 + + + + + + + |