aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/AddRefMan-pre.tex
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: