Chapter 10: Writing ad-hoc Tactics in Coq