From 33388d18f0165369a565cd5ca5b6eb153899271e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 19 Apr 2020 18:04:14 -0400
Subject: Fix the `with_strategy` tactic to work with `abstract`

---
 doc/sphinx/proof-engine/tactics.rst | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index fd6b2b3846..b376d9177f 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3370,7 +3370,9 @@ the conversion in hypotheses :n:`{+ @ident}`.
       Use this tactic with care, as effects do not persist past the
       end of the proof script.  Notably, this fine-tuning of the
       conversion strategy is not in effect during :cmd:`Qed` nor
-      :cmd:`Defined`, so this tactic is most useful to guard
+      :cmd:`Defined`, so this tactic is most useful either in
+      combination with :tacn:`abstract`, which will check the proof
+      early while the fine-tuning is still in effect, or to guard
       calls to conversion in tactic automation to ensure that, e.g.,
       :tacn:`unfold` does not fail just because the user made a
       constant :cmd:`Opaque`.
-- 
cgit v1.2.3