diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 10 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
4 files changed, 18 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 88a16e014c..096f4cae45 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3833,6 +3833,10 @@ Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. intros. exists (n // m). \end{coq_example} +\begin{coq_eval} +Clear Implicit Tactic. +Reset Initial. +\end{coq_eval} The tactic {\tt exists (n // m)} did not fail. The hole was solved by {\tt assumption} so that it behaved as {\tt exists (quo n m H)}. 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 + + + + + + + diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e6578ce52d..094cb6b19e 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -491,6 +491,8 @@ END VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF | [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ] +| [ "Clear" "Implicit" "Tactic" ] -> + [ Pfedit.clear_implicit_tactic () ] END |