Verified Commit 83ed79cb authored by Tej Chajed's avatar Tej Chajed
Browse files

Improve the IPM documentation

- Separated out the simpler invocations of tactics from their full
  forms. In the process we now document what parts of a tactic are
- 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
parent f0f9f3b6
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment