From 0b936be00d2c7c05d528b8d7304fc1e14d5546a5 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:41:46 +0000
Subject: 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
---
 doc/refman/RefMan-tac.tex | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc')

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)}.
-- 
cgit v1.2.3