Hi! I have a proof with two different subgoals that are solved by exactly the same proof script, which is long and I don't want to compact. I know of the `all:`

tactic, but is there something similar that allows me to solve two similar subgoals with a sub script?

is there a reason not to use number-based goal selectors? For example:

```
tac. 1-3,5,8-9,11: done.
```

I'm not familiar with that, can you point me to the documentation?

This may be it: https://coq.inria.fr/refman/proof-engine/ltac.html#grammar-token-range_selector

Thanks both!

Last updated: Jun 22 2024 at 14:01 UTC