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 Fomega terms. It is contributed by Jean-Christophe
Filliâtre and Pierre Letouzey.
- 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.