blob: 2f0b52834c422180f6a05b646bf1f894b27a48a7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
\addtocontents{sh}{BEGINADDENDUM=\thepage}
\coverpage{Addenddum to the Reference Manual}{\ }
\addcontentsline{toc}{part}{Additionnal documentation}
\setheaders{Presentation of the Addendum}
\section*{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.
\begin{description}
\item[Cases] This chapter details the use of generalized pattern-matching.
It is contributed by Cristina Cornes.
\item[Coercion] This chapter details the use of the coercion mechanism.
It is contributed by Amokrane Sa�bi.
\item[Extraction] This chapter explains how to extract in practice ML
files from $\FW$ terms.
\item[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.
\item[Omega] \texttt{Omega}, written by Pierre Cr�gut, solves a whole
class of arithmetic problems.
\item[Program] The \texttt{Program} technology intends to inverse the
extraction mechanism. It allows the developments of certified
programs in \Coq. This chapter is due to Catherine Parent.
\item[Ring] \texttt{Ring} is a tactic to do AC rewriting. This
chapter explains how to use it and how it works.
\end{description}
\atableofcontents
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
