Presentation of the Addendum
Presentation of the Addendum
Here you will find several pieces of additionnal 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.
- Cases
- This chapter details the use of generalized pattern-matching.
It is contributed by Cristina Cornes.
- Coercion
- This chapter details the use of the coercion mechanism.
It is contributed by Amokrane Saïbi.
- Extraction
- This chapter explains how to extract in practice ML
files from Fw terms.
- Natural
- This chapter is due to Yann Coscoy. It is the user
manual of the tools he wrote for printing proofs in natural
language. At this time, french and english languages are supported.
- Omega
- Omega, written by Pierre Crégut, solves a whole
class of arithmetic problems.
- Program
- The Program technology intends to inverse the
extraction mechanism. It allows the developpements of certified
programs in Coq. This chapter is due to Catherine Parent.
- Ring
- Ring is a tactic to do AC rewriting. This
chapter explains how to use it and how it works.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.1.9.html at 8/10/98