The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  Can someone point me at documentation / minimal example (or even the right keyword to google for this) for designing a Ltac

Ltac tac := ...

s.t.

"tac;" --> idtac "case 0"

"tac in H;" --> idtac H;

"tac in *;" --> idtac "all"

Thanks!