1 files changed, 0 insertions, 46 deletions
diff --git a/doc/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex
deleted file mode 100644
index d881329a..00000000
--- a/doc/rt/RefMan-cover.tex
+++ /dev/null
@@ -1,46 +0,0 @@
-\documentstyle[RRcover]{book}
-        % L'utilisation du style `french' force le résumé français à
-        % apparaître en premier.
-
-\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1}
-\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1
-\thanks
-{This research was partly supported by ESPRIT Basic Research
-Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
-}
-\RRauthor{Bruno Barras, Samuel Boutin, Cristina Cornes,
-Judica\"el Courant, Jean-Christophe Filli\^atre, Eduardo Gim\'enez,
-Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy,
-Catherine Parent, Christine Paulin-Mohring,
-Amokrane Sa{\"\i}bi, Benjamin Werner}
-\authorhead{}
-\titlehead{Coq V7.1 Reference Manual}
-\RRtheme{2}
-\RRprojet{Coq}
-\RRNo{0123456789}
-\RRdate{May 1997}
-%\RRpages{}
-\URRocq
-
-\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la
-v\'erification de preuves formelles dans une logique d'ordre
-sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
-Ce document constitue le manuel de r\'ef\'erence de la version V7.1
-qui est distribu\'ee par ftp anonyme à l'adresse
-\url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles,
-Calcul des Constructions Inductives}
-
-
-\RRabstract{Coq is a proof assistant based on a higher-order logic
-allowing powerful definitions of functions. 
-Coq V7.1 is available by anonymous
-ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
-Constructions}
-
-\begin{document}
-\makeRT
-\end{document}