Initial revision

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8143 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 46 insertions, 0 deletions

diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex
new file mode 100644
index 000000000..2f0b52834
--- /dev/null
+++ b/doc/AddRefMan-pre.tex
@@ -0,0 +1,46 @@
+\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: