From 6b223d1d668ecb76aa2609b7d6bb8a19e13136cd Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 9 May 2020 13:39:34 -0400
Subject: Revert "[with_strategy] Fix for coqchk"

This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18.

We instead add a warning in the manual and a kludge in the test-suite.
---
 doc/sphinx/proof-engine/tactics.rst | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7483ab3341..bc2168411b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3467,6 +3467,16 @@ the conversion in hypotheses :n:`{+ @ident}`.
       :tacn:`with_strategy` may not be robustly performant when
       scaling the size of the input.
 
+   .. warning::
+
+      In much the same way this tactic does not play well with
+      :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as
+      an intermediary, this tactic does not play well with ``coqchk``,
+      even when used with :tacn:`abstract`, due to the inability of
+      tactics to persist information about conversion hints in the
+      proof term. See `#12200
+      <https://github.com/coq/coq/issues/12200>`_ for more details.
+
 Conversion tactics applied to hypotheses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-- 
cgit v1.2.3