diff options
author | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
commit | 55ce117e8083477593cf1ff2e51a3641c7973830 (patch) | |
tree | a82defb4105f175c71b0d13cae42831ce608c4d6 /doc/rt/RefMan-cover.tex | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'doc/rt/RefMan-cover.tex')
-rw-r--r-- | doc/rt/RefMan-cover.tex | 46 |
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} |