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>

3 files changed, 24 insertions, 7 deletions

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"