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.