%\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: