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> --- plugins/ltac/tacintern.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'plugins/ltac/tacintern.ml') diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 597c3fdaac..929fd5e132 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -305,6 +305,12 @@ let intern_evaluable_reference_or_by_notation ist = function (Notation.interp_notation_as_global_reference ?loc GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) +let intern_smart_global ist = function + | {v=AN r} -> intern_global_reference ist r + | {v=ByNotation (ntn,sc);loc} -> + ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc + GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)) + (* Globalize a reduction expression *) let intern_evaluable ist r = let f ist r = @@ -813,6 +819,7 @@ let intern_ltac ist tac = let () = Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); + Genintern.register_intern0 wit_smart_global (lift intern_smart_global); Genintern.register_intern0 wit_ref (lift intern_global_reference); Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; -- cgit v1.2.3