Part: IV
Practical tools

• Chapter 11: The Coq commands
• Chapter 12: Utilities
• Chapter 13: ML-style pattern-matching
• Chapter 14: Implicit Coercions
• Chapter 15: Natural : proofs in natural language
• Chapter 16: Omega: a solver of quantifier-free problems in Presburger Arithmetic
• Chapter 17: The Program Tactic
• Chapter 18: Proof of imperative programs
• Chapter 19: Execution of extracted programs in Caml and Haskell
• Chapter 20: The Ring tactic