aboutsummaryrefslogtreecommitdiff
path: root/doc/title.tex
diff options
context:
space:
mode:
authormohring2004-01-06 16:52:44 +0000
committermohring2004-01-06 16:52:44 +0000
commitc1466b54d098e4e410aefacd6317bf8fa40bb63c (patch)
treee968766a88726210d0e4a8c2ed365b0366280d39 /doc/title.tex
parent3c94d3e2d09f6baa497aadba8f8c64bfd68a9ca9 (diff)
doc avec frames
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/title.tex')
-rwxr-xr-xdoc/title.tex5
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/title.tex b/doc/title.tex
index 53ad9e0f89..d332af0577 100755
--- a/doc/title.tex
+++ b/doc/title.tex
@@ -41,16 +41,16 @@ The Coq Proof Assistant\\
{\Large \bf LogiCal Project}\\
\vspace{15pt}
\end{center}
-
%BEGIN LATEX
\newpage
\vspace*{520pt}
\thispagestyle{empty}
%END LATEX
-
\begin{flushleft}
+%BEGIN LATEX
{\large{V\coqversion,
\printingdate}}\\[20pt]
+%END LATEX
{\large{\copyright INRIA 1999-2004}}\\
\end{flushleft}
%BEGIN LATEX
@@ -58,6 +58,7 @@ The Coq Proof Assistant\\
%END LATEX
}
+
\newcommand{\shorttitle}[1]{
\begin{center}
\begin{huge}