diff options
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/common/title.tex | 97 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 14 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 26 |
5 files changed, 69 insertions, 71 deletions
diff --git a/doc/common/title.tex b/doc/common/title.tex index 51e817cc5..83b5154fd 100755 --- a/doc/common/title.tex +++ b/doc/common/title.tex @@ -1,78 +1,69 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File title.tex -% Page formatting commands +% Page formatting commands % Macro \coverpage %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\setlength{\marginparwidth}{0pt} %\setlength{\oddsidemargin}{0pt} -%\setlength{\evensidemargin}{0pt} +%\setlength{\evensidemargin}{0pt} %\setlength{\marginparsep}{0pt} -%\setlength{\topmargin}{0pt} -%\setlength{\textwidth}{16.9cm} +%\setlength{\topmargin}{0pt} +%\setlength{\textwidth}{16.9cm} %\setlength{\textheight}{22cm} -\usepackage{fullpage} +%\usepackage{fullpage} -\newcommand{\printingdate}{\today} -\newcommand{\isdraft}{\Large\bf\today\\[20pt]} +%\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} +\bfseries % for the rest of this page, until \end{center} +\Huge +The Coq Proof Assistant\\[12pt] +#1\\[20pt] +\Large\today\\[20pt] +Version \coqversion\footnote[1]{This research was partly supported by IST working group ``Types''} + +\vspace{0pt plus .5fill} +#2 +\par\vfill +LogiCal Project + +\vspace*{15pt} \end{center} -%BEGIN LATEX \newpage -\vspace*{500pt} + \thispagestyle{empty} -%END LATEX +\hbox{}\vfill % without \hbox \vfill does not work at the top of the page \begin{flushleft} %BEGIN LATEX -{\large{V\coqversion, -\printingdate}}\\[20pt] +V\coqversion, \today +\par\vspace{20pt} %END LATEX -{\large{\copyright INRIA 1999-2004 ({\Coq} versions 7.x)}}\\ -{\large{\copyright INRIA 2004-2006 ({\Coq} versions 8.x)}}\\ -{\large{#3}} +\copyright INRIA 1999-2004 ({\Coq} versions 7.x) + +\copyright INRIA 2004-2006 ({\Coq} versions 8.x) + +#3 \end{flushleft} -%BEGIN LATEX -\newpage -%END LATEX -} +} % end of \coverpage definition -\newcommand{\shorttitle}[1]{ -\begin{center} -\begin{huge} -\begin{bf} -The Coq Proof Assistant\\ -\vspace{10pt} - #1\\ -\end{bf} -\end{huge} -\end{center} -\vspace{5pt} -} +% \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 @@ -80,7 +71,3 @@ The Coq Proof Assistant\\ % End: % $Id$ - - - - diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 8fdb8d8df..f0db1a0fb 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -251,7 +251,7 @@ Definition not (b:bool) := end. \end{coq_example} -can be alternatively written +\noindent can be alternatively written \begin{coq_eval} Reset not. diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 0beabc991..1ea680741 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -589,6 +589,7 @@ Coq-Club mailing list and bug-tracker systems, especially user groups from INRIA Rocquencourt, Radbout University, University of Pennsylvania and Yale University. +\enlargethispage{\baselineskip} \begin{flushright} Palaiseau, July 2006\\ Hugo Herbelin diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8331defbb..63f61ea8b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3299,14 +3299,14 @@ The tactic {\tt exists (n // m)} did not fail. The hole was solved by The {\tt Scheme} command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema: -\begin{tabbing} +\begin{quote} {\tt Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ with\\ - \mbox{}\hspace{0.1cm} \dots\ \\ + \mbox{}\hspace{0.1cm} \dots\\ with {\ident$_m$} := Induction for {\ident'$_m$} Sort {\sort$_m$}} -\end{tabbing} -\ident'$_1$ \dots\ \ident'$_m$ are different inductive type +\end{quote} +where \ident'$_1$ \dots\ \ident'$_m$ are different inductive type identifiers belonging to the same package of mutual inductive definitions. This command generates {\ident$_1$}\dots{} {\ident$_m$} to be mutually recursive definitions. Each term {\ident$_i$} proves a @@ -3353,14 +3353,14 @@ The {\tt Functional Scheme} command is a high-level experimental tool for generating automatically induction principles corresponding to (possibly mutually recursive) functions. Its syntax follows the schema: -\begin{tabbing} +\begin{quote} {\tt Functional Scheme {\ident$_1$} := Induction for \ident'$_1$ Sort {\sort$_1$} \\ with\\ \mbox{}\hspace{0.1cm} \dots\ \\ with {\ident$_m$} := Induction for {\ident'$_m$} Sort {\sort$_m$}} -\end{tabbing} -\ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function +\end{quote} +where \ident'$_1$ \dots\ \ident'$_m$ are different mutually defined function names (they must be in the same order as when they were defined). This command generates the induction principles \ident$_1$\dots\ident$_m$, following the recursive structure and case diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 34399196b..62c640b23 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -15,6 +15,7 @@ \usepackage{alltt} \usepackage{hevea} \usepackage{ifpdf} +\usepackage[headings]{fullpage} \usepackage{headers} % in this directory % for coqide @@ -30,20 +31,29 @@ \input{../common/version.tex} \input{../common/macros.tex}% extension .tex pour htmlgen \input{../common/title.tex}% extension .tex pour htmlgen - +%\input{headers} + +\usepackage[linktocpage,colorlinks]{hyperref} +% The manual advises to load hyperref package last to be able to redefine +% necessary commands. +% The above should work for both latex and pdflatex. Even if PDF is produced +% through DVI and PS using dvips and ps2pdf, hyperlinks should still work. +% linktocpage option makes page numbers, not section names, to be links in +% the table of contents. +% colorlinks option colors the links instead of using boxes. \begin{document} %BEGIN LATEX \sloppy\hbadness=5000 %END LATEX -\tophtml{} %BEGIN LATEX -\coverpage{Reference Manual}{The Coq Development Team} - {This material may be distributed only subject to the terms and - conditions set forth in the Open Publication License, v1.0 or later - (the latest version is presently available at - \ahrefurl{http://www.opencontent.org/openpub}). - Options A and B of the licence are {\em not} elected.} +\coverpage{Reference Manual} +{The Coq Development Team} +{This material may be distributed only subject to the terms and +conditions set forth in the Open Publication License, v1.0 or later +(the latest version is presently available at +\url{http://www.opencontent.org/openpub}). +Options A and B of the licence are {\em not} elected.} %END LATEX %\defaultheaders |