Make the IPM documentation more useful

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 argument to iModIntro is 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.