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