Several changes to make the IPM documentation more readable and useful as a reference:
- Separated out the simpler invocations of tactics from their full forms. In the process we now document what parts of a tactic are optional.
- Convey what the common and rare tactics are, for example that the
iModIntrois rarely needed.
- Use "destruct" to talk about invoking an intro pattern, rather than eliminate, to stay closer to Coq terminology and avoid this potentially confusing term for someone without the required logic/PL background.
- Added an overview of the "grammar entries" relevant to many tactics (ipat, selpat, spat, and pm_trm). Added links to those sections everywhere.
Really teaching the IPM can't be done here because it's a reference, so it notably lacks examples. I want to write a more tutorial or introductory version of this that actually illustrates the tactics and explains what you probably want to do, not just the full set of features.