- 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 PL term.
- Added an overview of the "grammar entries" relevant to many tactics
  (ipat, selpat, spat, and pm_trm). Added links to those sections
  everywhere.

Based om iris/iris!467 (comment 53064)
by @Blaisorblade.

This closes issue #305.

It now supports the specialization pattern `(H spat1 .. spatn)`, which first
recursively specializes the hypothesis `H` using the specialization patterns
`spat1 .. spatn`.

This commit closes issue #192.

This fixes issue #187.

sed -i 's/absolute/objective/g; s/relative/subjective/g; s/Absolute/Objective/g; s/Relative/Subjective/g' $(find ./ -name \*.v)