1 files changed, 62 insertions, 0 deletions
diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
new file mode 100644
index 00000000..461e8e6d
--- /dev/null
+++ b/doc/refman/AddRefMan-pre.tex
@@ -0,0 +1,62 @@
+%\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}
+
+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: