1 files changed, 46 insertions, 0 deletions
diff --git a/doc/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex
new file mode 100644
index 00000000..d881329a
--- /dev/null
+++ b/doc/rt/RefMan-cover.tex
@@ -0,0 +1,46 @@
+\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}