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>

2 files changed, 407 insertions, 0 deletions

diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out
index 952761acca..58931c4b82 100644
--- a/test-suite/output/print_ltac.out
+++ b/test-suite/output/print_ltac.out
@@ -6,3 +6,340 @@ Ltac t3 := idtacstr "my tactic"
 Ltac t4 x := match x with
              | ?A => (A, A)
              end
+The command has indeed failed with message:
+idnat is bound to a notation that does not denote a reference.
+Ltac withstrategy l x :=
+  let idx := smart_global:(id) in
+  let tl := strategy_level:(transparent) in
+  with_strategy
+  1
+  [
+  id
+  id
+  ]
+  with_strategy
+  l
+  [
+  id
+  id
+  ]
+  with_strategy
+  tl
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  ]
+  with_strategy
+  opaque
+  [
+  id
+  id
+  ]
+  with_strategy
+  expand
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  idx
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  x
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  x
+  ]
+  idtac
+The command has indeed failed with message:
+idnat is bound to a notation that does not denote a reference.
+Ltac withstrategy l x :=
+  let idx := smart_global:(id) in
+  let tl := strategy_level:(transparent) in
+  with_strategy
+  1
+  [
+  id
+  id
+  ]
+  with_strategy
+  l
+  [
+  id
+  id
+  ]
+  with_strategy
+  tl
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  ]
+  with_strategy
+  opaque
+  [
+  id
+  id
+  ]
+  with_strategy
+  expand
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  idx
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  x
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  ]
+  with_strategy
+  transparent
+  [
+  id
+  id
+  x
+  ]
+  idtac
+Ltac FE.withstrategy l x :=
+  let idx := smart_global:(FE.id) in
+  let tl := strategy_level:(transparent) in
+  with_strategy
+  1
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  l
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  tl
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  opaque
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  expand
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  transparent
+  [
+  idx
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  x
+  FE.id
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  FE.id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  x
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  FE.id
+  ]
+  with_strategy
+  transparent
+  [
+  FE.id
+  FE.id
+  x
+  ]
+  idtac
diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v
index a992846791..d0883e32e4 100644
--- a/test-suite/output/print_ltac.v
+++ b/test-suite/output/print_ltac.v
@@ -10,3 +10,73 @@ Print Ltac t3.
 (* https://github.com/coq/coq/issues/9716 *)
 Ltac t4 x := match x with ?A => constr:((A, A)) end.
 Print Ltac t4.
+
+Notation idnat := (@id nat).
+Notation idn := id.
+Notation idan := (@id).
+Fail Strategy transparent [idnat].
+Strategy transparent [idn].
+Strategy transparent [idan].
+Ltac withstrategy l x :=
+  let idx := smart_global:(id) in
+  let tl := strategy_level:(transparent) in
+  with_strategy 1 [id id] (
+  with_strategy l [id id] (
+  with_strategy tl [id id] (
+  with_strategy 0 [id id] (
+  with_strategy transparent [id id] (
+  with_strategy opaque [id id] (
+  with_strategy expand [id id] (
+  with_strategy 0 [idx] (
+  with_strategy 0 [id x] (
+  with_strategy 0 [x id] (
+  with_strategy 0 [idn] (
+  with_strategy 0 [idn x] (
+  with_strategy 0 [idn id] (
+  with_strategy 0 [idn id x] (
+  with_strategy 0 [idan] (
+  with_strategy 0 [idan x] (
+  with_strategy 0 [idan id] (
+  with_strategy 0 [idan id x] (
+  idtac
+    )))))))))))))))))).
+Print Ltac withstrategy.
+
+Module Type Empty. End Empty.
+Module E. End E.
+Module F (E : Empty).
+  Definition id {T} := @id T.
+  Notation idnat := (@id nat).
+  Notation idn := id.
+  Notation idan := (@id).
+  Fail Strategy transparent [idnat].
+  Strategy transparent [idn].
+  Strategy transparent [idan].
+  Ltac withstrategy l x :=
+    let idx := smart_global:(id) in
+    let tl := strategy_level:(transparent) in
+    with_strategy 1 [id id] (
+    with_strategy l [id id] (
+    with_strategy tl [id id] (
+    with_strategy 0 [id id] (
+    with_strategy transparent [id id] (
+    with_strategy opaque [id id] (
+    with_strategy expand [id id] (
+    with_strategy 0 [idx] (
+    with_strategy 0 [id x] (
+    with_strategy 0 [x id] (
+    with_strategy 0 [idn] (
+    with_strategy 0 [idn x] (
+    with_strategy 0 [idn id] (
+    with_strategy 0 [idn id x] (
+    with_strategy 0 [idan] (
+    with_strategy 0 [idan x] (
+    with_strategy 0 [idan id] (
+    with_strategy 0 [idan id x] (
+    idtac
+      )))))))))))))))))).
+  Print Ltac withstrategy.
+End F.
+
+Module FE := F E.
+Print Ltac FE.withstrategy.