7.16 Simple tactic macros
A simple example has more value than a long explanation:
Coq < Tactic Definition Solve := [<:tactic:<Simpl; Intros; Auto>>].
Coq < Tactic Definition ElimBoolRewrite [$b $H1 $H2] :=
Coq < [<:tactic:<Elim $b;
Coq < [Intros; Rewrite $H1; EAuto | Intros; Rewrite $H2; EAuto ]>>].
Those tactic definitions are just macros, they behave like the
syntactic definitions in the tactic world. The right side of the
definition is an AST (see page X),
but you can type a command if you
enclose it between << >>
or <:command:< >>
, and you can
type a tactic script (the most frequent case) if you enclose it
between <:tactic:< >>
.
The tactics macros are synchronous with the Coq section mechanism:
a Tactic Definition is deleted from the current environment
when you close the section (see also 2.5)
where it was defined. If you want that a
tactic macro defined in a module is usable in the modules that
require it, you should put it outside of any section.
This command is designed to be simple, so the user who wants to do
complicate things with it should better read the chapter
10 about the user-defined tactics.