Tactics and automation

The complete sources of this chapter

Exercises

Errata

  1. Page 195, section 7.3.2:
    read: "The subst tactic looks for hypotheses of the form x = exp or exp = x "
  2. Page 196, end of the first paragraph: read: "It is however, a good complement to our caseEq tactic ..."
  3. Section 7.1.2.2, paragraph 2, page 189:
    read "Moreover, the argument delta" instead of "Moreover, the argument Delta"
  4. Page 209. "[|- context [(S ?1)]]" should be replaced by "[|- context [(S ?X1)]]"
  5. Page 209 (fifth paragraph) replace "match ?1" by "match X1"
  6. Page 210 (last paragraph) read "simpl_on" instead of "simpl_On"
  7. Section 7.6.2.1, page 203:
    read "The patterns have the form
    [h1:t1, h2:t2, ... |- C]"
    (instead of [h1:t1; h2:t2, ... |- C]