Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 86 insertions, 0 deletions

diff --git a/doc/common/title.tex b/doc/common/title.tex
new file mode 100755
index 00000000..2ed49ede
--- /dev/null
+++ b/doc/common/title.tex
@@ -0,0 +1,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 $ 
+
+
+
+