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

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