\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[Cases] This chapter details the use of generalized pattern-matching.
  It is contributed by Cristina Cornes.

\item[Coercion] This chapter details the use of the coercion mechanism.
  It is contributed by Amokrane Saïbi.

\item[Extraction] This chapter explains how to extract in practice ML
  files from $\FW$ terms. 

\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.

\item[Ring] \texttt{Ring} is a tactic to do AC rewriting. This
  chapter explains how to use it and how it works.

\end{description}

\atableofcontents


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: