7.16 A Simple way to define 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.