From 55ce117e8083477593cf1ff2e51a3641c7973830 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 13 Feb 2007 13:48:12 +0000
Subject: Imported Upstream version 8.1+dfsg

---
 doc/refman/AddRefMan-pre.tex | 58 --------------------------------------------
 1 file changed, 58 deletions(-)
 delete mode 100644 doc/refman/AddRefMan-pre.tex

(limited to 'doc/refman/AddRefMan-pre.tex')

diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex
deleted file mode 100644
index 5312b8fc..00000000
--- a/doc/refman/AddRefMan-pre.tex
+++ /dev/null
@@ -1,58 +0,0 @@
-%\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: 
-- 
cgit v1.2.3

