← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/rt/RefMan-cover.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/rt/RefMan-cover.tex
 
1
\documentstyle[RRcover]{book}
 
2
        % L'utilisation du style `french' force le r�sum� fran�ais �
 
3
        % appara�tre en premier.
 
4
 
 
5
\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1}
 
6
\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1
 
7
\thanks
 
8
{This research was partly supported by ESPRIT Basic Research
 
9
Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
 
10
}
 
11
\RRauthor{Bruno Barras, Samuel Boutin, Cristina Cornes,
 
12
Judica\"el Courant, Jean-Christophe Filli\^atre, Eduardo Gim\'enez,
 
13
Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy,
 
14
Catherine Parent, Christine Paulin-Mohring,
 
15
Amokrane Sa{\"\i}bi, Benjamin Werner}
 
16
\authorhead{}
 
17
\titlehead{Coq V7.1 Reference Manual}
 
18
\RRtheme{2}
 
19
\RRprojet{Coq}
 
20
\RRNo{0123456789}
 
21
\RRdate{May 1997}
 
22
%\RRpages{}
 
23
\URRocq
 
24
 
 
25
\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la
 
26
v\'erification de preuves formelles dans une logique d'ordre
 
27
sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
 
28
Ce document constitue le manuel de r\'ef\'erence de la version V7.1
 
29
qui est distribu\'ee par ftp anonyme � l'adresse
 
30
\url{ftp://ftp.inria.fr/INRIA/coq/}}
 
31
 
 
32
\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles,
 
33
Calcul des Constructions Inductives}
 
34
 
 
35
 
 
36
\RRabstract{Coq is a proof assistant based on a higher-order logic
 
37
allowing powerful definitions of functions. 
 
38
Coq V7.1 is available by anonymous
 
39
ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
 
40
 
 
41
\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
 
42
Constructions}
 
43
 
 
44
\begin{document}
 
45
\makeRT
 
46
\end{document}