blob: 27651709a510b1fa9d50aabdd215d7b074fd86a1 (
plain)
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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% File title.tex
% Page formatting commands
% Macro \coverpage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\setlength{\marginparwidth}{0pt}
%\setlength{\oddsidemargin}{0pt}
%\setlength{\evensidemargin}{0pt}
%\setlength{\marginparsep}{0pt}
%\setlength{\topmargin}{0pt}
%\setlength{\textwidth}{16.9cm}
%\setlength{\textheight}{22cm}
\usepackage{fullpage}
\newcommand{\printingdate}{\today}
\newcommand{\isdraft}{\Large\bf\today\\[20pt]}
%\newcommand{\isdraft}{\vspace{20pt}}
%To show the top for the toc in html
\newcommand{\tophtml}{}
\newcommand{\coverpage}[2]{
\thispagestyle{empty}
\begin{center}
\begin{Huge}
\begin{bf}
The Coq Proof Assistant\\
\vspace{12pt}
#1\\
\end{bf}
\end{Huge}
\vspace{20pt}
\isdraft
{\Large \bf Version \coqversion}
\footnote[1]{This research was partly supported by ESPRIT Basic Research
Action ``Types''}
% Obsolete CP {and by the GDR ``Programmation'' co-financed by MRE-PRC
% and CNRS.}
\\
\vspace{120pt}
{\bf #2}\\
\vfill
{\Large \bf LogiCal Project}\\
\vspace{15pt}
\end{center}
\newpage
\vspace*{520pt}
\thispagestyle{empty}
\begin{flushleft}
{\large{V7.4,
\printingdate}}\\[20pt]
{\large{\copyright INRIA 1999-2002}}\\
\end{flushleft}
\newpage}
\newcommand{\shorttitle}[1]{
\begin{center}
\begin{huge}
\begin{bf}
The Coq Proof Assistant\\
\vspace{10pt}
#1\\
\end{bf}
\end{huge}
\end{center}
\vspace{5pt}
}
% Local Variables:
% mode: LaTeX
% TeX-master: ""
% End:
% $Id$
|
