summaryrefslogtreecommitdiff
path: root/doc/refman/AddRefMan-pre.tex
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /doc/refman/AddRefMan-pre.tex
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'doc/refman/AddRefMan-pre.tex')
-rw-r--r--doc/refman/AddRefMan-pre.tex58
1 files changed, 58 insertions, 0 deletions
diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
new file mode 100644
index 00000000..5312b8fc
--- /dev/null
+++ b/doc/refman/AddRefMan-pre.tex
@@ -0,0 +1,58 @@
+%\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: