1. 06 Dec, 2020 1 commit
  2. 04 Dec, 2020 1 commit
  3. 03 Dec, 2020 1 commit
    • 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
  4. 29 Oct, 2020 1 commit
  5. 29 Sep, 2020 1 commit
  6. 29 Jun, 2020 1 commit
  7. 22 May, 2020 1 commit
  8. 07 Apr, 2020 3 commits
  9. 20 Mar, 2020 1 commit
  10. 18 Feb, 2020 5 commits
  11. 19 Dec, 2019 1 commit
  12. 01 Nov, 2019 1 commit
  13. 11 Sep, 2019 2 commits
  14. 16 Aug, 2019 1 commit
  15. 01 May, 2019 3 commits
  16. 23 Apr, 2019 1 commit
  17. 17 Apr, 2019 1 commit
  18. 16 Feb, 2019 1 commit
  19. 23 Jan, 2019 1 commit
  20. 14 Jan, 2019 1 commit
  21. 11 Jan, 2019 2 commits
  22. 25 Dec, 2018 1 commit
  23. 30 May, 2018 1 commit
  24. 18 May, 2018 1 commit
  25. 04 Mar, 2018 1 commit
  26. 03 Mar, 2018 1 commit
  27. 28 Feb, 2018 1 commit
  28. 23 Feb, 2018 2 commits
  29. 19 Feb, 2018 1 commit