blob: 856a823de04d8bd3ef7af2af82768e4200af4bb4 (
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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
%\coverpage{Addendum to the Reference Manual}{\ }
%\addcontentsline{toc}{part}{Additional documentation}
%BEGIN LATEX
\setheaders{Presentation of the Addendum}
%END LATEX
\chapter*{Presentation of the Addendum}
%HEVEA\cutname{addendum.html}
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[Extended pattern-matching] This chapter details the use of
generalized pattern-matching. It is contributed by Cristina Cornes
and Hugo Herbelin.
\item[Implicit coercions] This chapter details the use of the coercion
mechanism. It is contributed by Amokrane Saïbi.
%\item[Proof of imperative programs] This chapter explains how to
% prove properties of annotated programs with imperative features.
% It is contributed by Jean-Christophe Filliâtre
\item[Program extraction] This chapter explains how to extract in practice ML
files from $\FW$ terms. It is contributed by Jean-Christophe
Filliâtre and Pierre Letouzey.
\item[Program] This chapter explains the use of the \texttt{Program}
vernacular which allows the development of certified
programs in \Coq. It is contributed by Matthieu Sozeau and replaces
the previous \texttt{Program} tactic by Catherine Parent.
%\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[The {\tt 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.
\item[The {\tt 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.
\item[Calling external provers] This chapter describes several tactics
which call external provers.
\end{description}
\atableofcontents
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
