← Back to branch summary

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

« back to all changes in this revision

Viewing changes to 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:
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}