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.