blob: 5312b8fc2fe17f4261189ca5956ce704ba099d31 (
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
|
%\coverpage{Addendum to the Reference Manual}{\ }
%\addcontentsline{toc}{part}{Additional documentation}
\setheaders{Presentation of the Addendum}
\chapter*{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[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[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. {\bf This
% feature is not available in {\Coq} version 7.}
\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.
\end{description}
\atableofcontents
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
