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> --- vernac/g_vernac.mlg | 6 ------ 1 file changed, 6 deletions(-) (limited to 'vernac') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3cb10364b5..049c3a0844 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -790,12 +790,6 @@ GRAMMAR EXTEND Gram { List.map (fun name -> (name.CAst.v, MaxImplicit)) items } ] ]; - strategy_level: - [ [ IDENT "expand" -> { Conv_oracle.Expand } - | IDENT "opaque" -> { Conv_oracle.Opaque } - | n=integer -> { Conv_oracle.Level n } - | IDENT "transparent" -> { Conv_oracle.transparent } ] ] - ; instance_name: [ [ name = ident_decl; bl = binders -> { (CAst.map (fun id -> Name id) (fst name), snd name), bl } -- cgit v1.2.3