Stream: Coq users

Topic: ✔ Is it possible to generalize multiple vars in a single ...

Daniel Hilst Selli (Dec 29 2021 at 02:40):

I'm doing generalize dependent a. generalize dependent b is there anything like generalize dependent a, b?

Li-yao (Dec 29 2021 at 03:20):

There's revert a b although you have to also mention the hypotheses that depend on those variables, and otherwise you can define your own tactic Ltac gd2 a b := generalize dependent a; generalize dependent b.

Daniel Hilst Selli (Dec 29 2021 at 17:37):

Hmm a custom tactic is a good idea, thank you!

Last updated: Sep 26 2023 at 13:01 UTC