Add a `with_strategy` tactic

Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.

We have some timeouts in the strategy success file.  We should not run
into issues, because we are not really testing how long these take.  We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.

Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.

One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556

Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>

1 files changed, 20 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 8989dd29ab..fd6b2b3846 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3355,6 +3355,26 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This is the most general syntax that combines the different variants.
 
+.. tacn:: with_strategy @strategy_level_or_var [ {+ @smart_qualid } ] @ltac_expr3
+   :name: with_strategy
+
+   Executes :token:`ltac_expr3`, applying the alternate unfolding
+   behavior that the :cmd:`Strategy` command controls, but only for
+   :token:`ltac_expr3`.  This can be useful for guarding calls to
+   reduction in tactic automation to ensure that certain constants are
+   never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to
+   ensure that unfolding does not fail.
+
+   .. note::
+
+      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
+      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`.
+
 Conversion tactics applied to hypotheses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~