1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
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}
|
