# Coq Reference Manual

# Presentation of the Addendum

Here you will find several pieces of additional documentation for the Coq Reference Manual. Each of this chapters is concentrated on a particular topic, that should interest only a fraction of the Coq users: that’s the reason why they are apart from the Reference Manual.

Extended pattern-matching
  This chapter details the use of generalized pattern-matching. It is contributed by Cristina Cornes and Hugo Herbelin.
Implicit coercions
  This chapter details the use of the coercion mechanism. It is contributed by Amokrane Saïbi.
Program extraction
  This chapter explains how to extract in practice ML files from Fω terms. It is contributed by Jean-Christophe Filliâtre and Pierre Letouzey.
Program
  This chapter explains the use of the Program vernacular which allows the development of certified programs in Coq. It is contributed by Matthieu Sozeau and replaces the previous Program tactic by Catherine Parent.
omega
  omega, written by Pierre Crégut, solves a whole class of arithmetic problems.
The ring tactic
  This is a tactic to do AC rewriting. This chapter explains how to use it and how it works. The chapter is contributed by Patrick Loiseleur.
The Setoid_replace tactic
  This is a tactic to do rewriting on types equipped with specific (only partially substitutive) equality. The chapter is contributed by Clément Renard.
Calling external provers
  This chapter describes several tactics which call external provers.