1. 10 Dec, 2020 1 commit
  2. 09 Dec, 2020 2 commits
  3. 07 Dec, 2020 6 commits
  4. 06 Dec, 2020 14 commits
  5. 04 Dec, 2020 14 commits
  6. 03 Dec, 2020 3 commits
    • Tej Chajed's avatar
      Improve the IPM documentation · 83ed79cb
      Tej Chajed authored
      - 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.
      83ed79cb
    • Ralf Jung's avatar
      Merge branch 'fix-hint-locality' into 'master' · fb2b600c
      Ralf Jung authored
      Add explicit Local/Global to hints at top level
      
      See merge request !594
      fb2b600c
    • Tej Chajed's avatar
      eb376fae