Stream: Coq users

Topic: Tactic to return the whole goal?

view this post on Zulip Daniel Hilst Selli (Aug 23 2022 at 20:26):

some times I write a tactic that walk over an expression and when I want to apply it to the whole goal I do something like this

match goal with
| |- ?goal => my_tactic goal

Is there a better alternative to get the whole goal without this match?

view this post on Zulip Paolo Giarrusso (Aug 24 2022 at 02:17):

That seems good

Last updated: Jun 22 2024 at 15:01 UTC