Stream: Coq users

Topic: Tactic to return the whole goal?

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
end.

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

Paolo Giarrusso (Aug 24 2022 at 02:17):

That seems good

Last updated: Sep 23 2023 at 06:01 UTC