Part: III
User extensions

• Chapter 9: Syntax extensions
• Chapter 10: Writing ad-hoc Tactics in Coq