From 2edbbfee7fdcfb2a4804524091930c5dab7b9db4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 19 Apr 2020 17:37:27 -0400 Subject: 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 Co-Authored-By: Théo Zimmermann Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> --- doc/tools/docgram/orderedGrammar | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'doc/tools/docgram/orderedGrammar') 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" -- cgit v1.2.3