Part: IV
Practical tools
Chapter 11: The
Coq
commands
Chapter 12: Utilities
Chapter 13: Extended pattern-matching
Chapter 14: Implicit Coercions
Chapter 15:
Omega
: a solver of quantifier-free problems in Presburger Arithmetic
Chapter 16: Proof of imperative programs
Chapter 17: Extraction of programs in Objective Caml and Haskell
Chapter 18: The
Ring
tactic
Chapter 19: The
Setoid_replace
tactic