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.

1 files changed, 10 insertions, 0 deletions

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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~