Make the IPM documentation more useful

Merged Tej Chajed requested to merge tchajed/iris-coq:revamp-ipm-docs into master

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.

Edited by Tej Chajed

Merge request reports