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>

7 files changed, 82 insertions, 18 deletions

diff --git a/doc/changelog/04-tactics/12129-add-with-strategy.rst b/doc/changelog/04-tactics/12129-add-with-strategy.rst
new file mode 100644
index 0000000000..68558c0cf4
--- /dev/null
+++ b/doc/changelog/04-tactics/12129-add-with-strategy.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  New tactical :tacn:`with_strategy` added which behaves like the
+  command :cmd:`Strategy`, with effects local to the given tactic
+  (`#12129 <https://github.com/coq/coq/pull/12129>`_, by Jason Gross).
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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 1759264e87..7191444bac 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -817,13 +817,15 @@ described first.
 
 .. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] }
 
-   .. insertprodn strategy_level strategy_level
+   .. insertprodn strategy_level strategy_level_or_var
 
    .. prodn::
       strategy_level ::= opaque
       | @int
       | expand
       | transparent
+      strategy_level_or_var ::= @strategy_level
+      | @ident
 
    This command accepts the :attr:`local` attribute, which limits its effect
    to the current section or module, in which case the section and module
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index d72409e0d9..ea5ad79a80 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1714,6 +1714,11 @@ Tactic notations allow customizing the syntax of tactics.
         - a global reference of term
         - :tacn:`unfold`
 
+      * - ``smart_global``
+        - :token:`smart_qualid`
+        - a global reference of term
+        - :tacn:`with_strategy`
+
       * - ``constr``
         - :token:`term`
         - a term
@@ -1734,6 +1739,16 @@ Tactic notations allow customizing the syntax of tactics.
         - an integer
         - :tacn:`do`
 
+      * - ``strategy_level``
+        - :token:`strategy_level`
+        - a strategy level
+        -
+
+      * - ``strategy_level_or_var``
+        - :token:`strategy_level_or_var`
+        - a strategy level
+        - :tacn:`with_strategy`
+
       * - ``tactic``
         - :token:`ltac_expr`
         - a tactic
@@ -1766,18 +1781,24 @@ Tactic notations allow customizing the syntax of tactics.
 
    .. todo: notation doesn't support italics
 
-   .. note:: In order to be bound in tactic definitions, each syntactic
-             entry for argument type must include the case of a simple |Ltac|
-             identifier as part of what it parses. This is naturally the case for
-             ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``.
-             This is the reason for introducing a special entry ``int_or_var`` which
-             evaluates to integers only but which syntactically includes
+   .. note:: In order to be bound in tactic definitions, each
+             syntactic entry for argument type must include the case
+             of a simple |Ltac| identifier as part of what it
+             parses. This is naturally the case for ``ident``,
+             ``simple_intropattern``, ``reference``, ``constr``, ...
+             but not for ``integer`` nor for ``strategy_level``.  This
+             is the reason for introducing special entries
+             ``int_or_var`` and ``strategy_level_or_var`` which
+             evaluate to integers or strategy levels only,
+             respectively, but which syntactically includes
              identifiers in order to be usable in tactic definitions.
 
-   .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` entries can be used in
-             primitive tactics or in other notations at places where a list of the
-             underlying entry can be used: entry is either ``constr``, ``hyp``, ``integer``
-             or ``int_or_var``.
+   .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*``
+             entries can be used in primitive tactics or in other
+             notations at places where a list of the underlying entry
+             can be used: entry is either ``constr``, ``hyp``,
+             ``integer``, ``smart_qualid``, ``strategy_level``,
+             ``strategy_level_or_var``, or ``int_or_var``.
 
 
 .. rubric:: Footnotes
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index c7e3ee18ad..62cc8ea86b 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1839,3 +1839,7 @@ sentence: [
 document: [
 | LIST0 sentence
 ]
+
+strategy_level: [
+| DELETE strategy_level0
+]
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 4274dccb40..92e9df51d5 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -451,6 +451,14 @@ bar_cbrace: [
 | test_pipe_closedcurly "|" "}"
 ]
 
+strategy_level: [
+| "expand"
+| "opaque"
+| integer
+| "transparent"
+| strategy_level0
+]
+
 vernac_toplevel: [
 | "Drop" "."
 | "Quit" "."
@@ -1213,13 +1221,6 @@ more_implicits_block: [
 | "{" LIST1 name "}"
 ]
 
-strategy_level: [
-| "expand"
-| "opaque"
-| integer
-| "transparent"
-]
-
 instance_name: [
 | ident_decl binders
 |
@@ -1598,6 +1599,7 @@ simple_tactic: [
 | "guard" test
 | "decompose" "[" LIST1 constr "]" constr
 | "optimize_heap"
+| "with_strategy" strategy_level_or_var "[" LIST1 smart_global "]" tactic3
 | "eassumption"
 | "eexact" constr
 | "trivial" auto_using hintbases
@@ -1855,6 +1857,11 @@ test_lpar_id_colon: [
 | local_test_lpar_id_colon
 ]
 
+strategy_level_or_var: [
+| strategy_level
+| identref
+]
+
 comparison: [
 | "="
 | "<"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index df4e5a22e3..11f06b7b8a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -659,6 +659,11 @@ strategy_level: [
 | "transparent"
 ]
 
+strategy_level_or_var: [
+| strategy_level
+| ident
+]
+
 reserv_list: [
 | LIST1 ( "(" simple_reserv ")" )
 | simple_reserv
@@ -1234,6 +1239,7 @@ simple_tactic: [
 | "guard" int_or_var comparison int_or_var
 | "decompose" "[" LIST1 one_term "]" one_term
 | "optimize_heap"
+| "with_strategy" strategy_level_or_var "[" LIST1 smart_qualid "]" ltac_expr3
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
 | "reset" "ltac" "profile"