7.15 Simple tactic macros

A simple example has more value than a long explanation:

Coq < Tactic Definition Solve := Simpl; Intros; Auto.
Current goal aborted

Coq < Tactic Definition ElimBoolRewrite b H1 H2 := 
Coq <   Elim b; 
Coq <   [Intros; Rewrite H1; EAuto | Intros; Rewrite H2; EAuto ].
Solve is defined

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.4) 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.

The chapter 10 gives examples of more complex user-defined tactics.