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