diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 10 |
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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |