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
81
82
83
84
85
86
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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}[3]{
\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 IST working group ``Types''}
\\
\vspace{120pt}
{\bf #2}\\
\vfill
{\Large \bf LogiCal Project}\\
\vspace{15pt}
\end{center}
%BEGIN LATEX
\newpage
\vspace*{500pt}
\thispagestyle{empty}
%END LATEX
\begin{flushleft}
%BEGIN LATEX
{\large{V\coqversion,
\printingdate}}\\[20pt]
%END LATEX
{\large{\copyright INRIA 1999-2004 ({\Coq} versions 7.x)}}\\
{\large{\copyright INRIA 2004-2006 ({\Coq} versions 8.x)}}\\
{\large{#3}}
\end{flushleft}
%BEGIN LATEX
\newpage
%END LATEX
}
\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: title.tex 8607 2006-02-23 14:21:14Z herbelin $
|
