I'm planning to demonstrate Coq tactics to some graduate students studying type theory, and recently it seemed that many of the tactics could be re-defined with `refine`

: (feedback welcome) https://gist.github.com/siraben/d66cc482a5f38d8f80430932e62f7957

However, how would I implement someting like `generalize dependent`

using Ltac + refine?

All tactics boil down to refine. `generalize dependent x`

should be `refine (_ H1 .. Hn x)`

where `H1 .. Hn`

are the hypothesis in which `x`

occurs.

@Enrico Tassi do you need to clear `H1 ... Hn`

too?

Yes, and also `x`

Last updated: Jan 27 2023 at 02:04 UTC