diff options
author | 2003-12-10 13:12:31 +0000 | |
---|---|---|
committer | 2003-12-10 13:12:31 +0000 | |
commit | 265d773ab32168fc1ae675332ed6a0e6df18080b (patch) | |
tree | 7d4f7c875d8cb4dbbf3bd87fb2b8bf04764570f2 | |
parent | e31e599f5cd5e539987c2741fece8bb9474dbbc6 (diff) |
presentation, biblio;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8381 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/AddRefMan-pre.tex | 2 | ||||
-rw-r--r-- | doc/Correctness.tex | 2 | ||||
-rw-r--r-- | doc/Makefile | 2 | ||||
-rw-r--r-- | doc/RefMan-ext.tex | 2 | ||||
-rw-r--r-- | doc/RefMan-ide.tex | 3 | ||||
-rwxr-xr-x | doc/RefMan-lib.tex | 4 | ||||
-rwxr-xr-x | doc/RefMan-pre.tex | 3 | ||||
-rwxr-xr-x | doc/RefMan-uti.tex | 2 | ||||
-rw-r--r-- | doc/Reference-Manual.tex | 7 | ||||
-rwxr-xr-x | doc/biblio.bib | 185 | ||||
-rw-r--r-- | doc/headers.tex | 2 |
11 files changed, 131 insertions, 83 deletions
diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex index d467b84e6..3ddf2e0c5 100644 --- a/doc/AddRefMan-pre.tex +++ b/doc/AddRefMan-pre.tex @@ -1,4 +1,6 @@ +%BEGIN LATEX \RefManCutCommand{BEGINADDENDUM=\thepage} +%END LATEX \coverpage{Addenddum to the Reference Manual}{\ } \addcontentsline{toc}{part}{Additional documentation} \setheaders{Presentation of the Addendum} diff --git a/doc/Correctness.tex b/doc/Correctness.tex index a5e378199..98c5c4568 100644 --- a/doc/Correctness.tex +++ b/doc/Correctness.tex @@ -20,7 +20,7 @@ This chapter describes a tactic to prove the correctness and termination of imperative programs annotated in a Floyd-Hoare logic style. The theoretical fundations of this tactic are described -in~\cite{Filliatre99,Filliatre00a}. +in~\cite{Filliatre99,Filliatre03jfp}. This tactic is provided in the \Coq\ module \texttt{Correctness}, which does not belong to the initial state of \Coq. So you must import it when necessary, with the following command: diff --git a/doc/Makefile b/doc/Makefile index 3e1e14f81..aac7fbda8 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -23,7 +23,7 @@ COQWEBSTY=/usr/share/texmf/tex/latex/misc/ HEVEALIB=/usr/local/lib/hevea LATEX=latex -BIBTEX=bibtex +BIBTEX=bibtex -min-crossref=10 MAKEINDEX=makeindex PDFLATEX=pdflatex diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex index 9f66c2850..223585d54 100644 --- a/doc/RefMan-ext.tex +++ b/doc/RefMan-ext.tex @@ -1031,7 +1031,7 @@ only the structure declared first as canonical is considered. \begin{Variants} \item {\tt Canonical Structure {\ident} := {\term} : {\type}.}\\ {\tt Canonical Structure {\ident} := {\term}.}\\ - {\tt Canonical Structure {\ident} : {\type} := {\term}.}\\ + {\tt Canonical Structure {\ident} : {\type} := {\term}.} These are equivalent to a regular definition of {\ident} followed by the declaration diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex index 02b82985d..5fa42d571 100644 --- a/doc/RefMan-ide.tex +++ b/doc/RefMan-ide.tex @@ -17,11 +17,14 @@ obviously no meaning for \coqide{} being ignored. \begin{figure}[t] \begin{center} +%HEVEA\imgsrc{coqide.png} +%BEGIN LATEX \ifx\pdfoutput\undefined % si on est pas en pdflatex \includegraphics[width=1.0\textwidth]{coqide.eps} \else \includegraphics[width=1.0\textwidth]{coqide.png} \fi +%END LATEX \end{center} \caption{Coqide main screen} \label{fig:coqide} diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex index 88cbbc57d..1b75c92a3 100755 --- a/doc/RefMan-lib.tex +++ b/doc/RefMan-lib.tex @@ -1035,7 +1035,9 @@ Goal forall x y z:R, (x * y * z)%R <> 0%R. intros; split_Rmult. \end{coq_example} -All this tactics has been written with the new tactic language.\\ +All this tactics has been written with the new tactic language. + +\bigskip More details are available in this document: {\tt http://coq.inria.fr/$\sim$desmettr/Reals.ps}.\\ diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex index 4b47c5028..36a10f664 100755 --- a/doc/RefMan-pre.tex +++ b/doc/RefMan-pre.tex @@ -382,7 +382,8 @@ contributed by Jean Goubault was integrated in the basic theories. Jacek Chrz\k{a}szcz designed and implemented the module system of {\Coq} whose foundations are in Judicaël Courant's PhD thesis. -\\ + +\bigskip The development was coordinated by C. Paulin. diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex index 0c594cfab..9a598b193 100755 --- a/doc/RefMan-uti.tex +++ b/doc/RefMan-uti.tex @@ -274,7 +274,9 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and {\tt coq-tex}. Man pages are installed at installation time (see installation instructions in file {\tt INSTALL}, step 6). +%BEGIN LATEX \RefManCutCommand{ENDREFMAN=\thepage} +%END LATEX % $Id$ diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index 493619166..f272a04f6 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -25,6 +25,8 @@ \input{./headers.tex}% extension .tex pour htmlgen \begin{document} +\sloppy\hbadness=3500 + \tophtml{} \coverpage{Reference Manual}{The Coq Development Team} @@ -71,16 +73,19 @@ \include{Extraction.v}% \include{Polynom.v}% = Ring \include{Setoid.v}% Tactique pour les setoides +%BEGIN LATEX \RefManCutCommand{ENDADDENDUM=\thepage} - +%END LATEX \nocite{*} \bibliographystyle{plain} \bibliography{biblio} +%BEGIN LATEX \RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps} \RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps} \RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-} \RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM} \RefManCutClose +%END LATEX \printindex diff --git a/doc/biblio.bib b/doc/biblio.bib index 3e1d96344..242eebd4e 100755 --- a/doc/biblio.bib +++ b/doc/biblio.bib @@ -1,6 +1,8 @@ -@STRING{toappear="To appear"} +@string{jfp = "Journal of Functional Programming"} @STRING{lncs="Lecture Notes in Computer Science"} +@STRING{lnai="Lecture Notes in Artificial Intelligence"} +@string{SV = "{Sprin\-ger-Verlag}"} @INPROCEEDINGS{Aud91, AUTHOR = {Ph. Audebaud}, @@ -59,13 +61,6 @@ Computer Architecture}, YEAR = {1991} } -@BOOK{Bastad92, - EDITOR = {B. Nordstr\"om and K. Petersson and G. Plotkin}, - PUBLISHER = {Available by ftp at site ftp.inria.fr}, - TITLE = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, - YEAR = {1992} -} - @ARTICLE{BeKe92, AUTHOR = {G. Bellin and J. Ketonen}, JOURNAL = {Theoretical Computer Science}, @@ -77,7 +72,7 @@ Computer Architecture}, @BOOK{Bee85, AUTHOR = {M.J. Beeson}, - PUBLISHER = {Springer-Verlag}, + PUBLISHER = SV, TITLE = {Foundations of Constructive Mathematics, Metamathematical Studies}, YEAR = {1985} } @@ -112,7 +107,8 @@ s}, author = {S. Boutin}, booktitle = {TACS'97}, editor = {Martin Abadi and Takahashi Ito}, - publisher = {LNCS, Springer-Verlag}, + publisher = SV, + series = lncs, volume=1281, PS={http://pauillac.inria.fr/~boutin/public_w/submitTACS97.ps.gz}, year = {1997} @@ -183,8 +179,8 @@ s}, ADDRESS = {Berg en Dal, The Netherlands}, TITLE = {Mathematical Quotients and Quotient Types in Coq}, BOOKTITLE = {TYPES'02}, - PUBLISHER = {Springer-Verlag}, - SERIES = {LNCS}, + PUBLISHER = SV, + SERIES = LNCS, VOLUME = {2646}, YEAR = {2003} } @@ -201,8 +197,8 @@ s}, AUTHOR = {Th. Coquand and G. Huet}, ADDRESS = {Linz}, BOOKTITLE = {EUROCAL'85}, - PUBLISHER = {Springer-Verlag}, - SERIES = {LNCS}, + PUBLISHER = SV, + SERIES = LNCS, TITLE = {{Constructions : A Higher Order Proof System for Mechanizing Mathematics}}, VOLUME = {203}, YEAR = {1985} @@ -230,8 +226,8 @@ s}, AUTHOR = {Th. Coquand and C. Paulin-Mohring}, BOOKTITLE = {Proceedings of Colog'88}, EDITOR = {P. Martin-L\"of and G. Mints}, - PUBLISHER = {Springer-Verlag}, - SERIES = {LNCS}, + PUBLISHER = SV, + SERIES = LNCS, TITLE = {Inductively defined types}, VOLUME = {417}, YEAR = {1990} @@ -281,7 +277,6 @@ s}, @INPROCEEDINGS{Coq92, AUTHOR = {Th. Coquand}, - BOOKTITLE = {in \cite{Bastad92}}, TITLE = {{Pattern Matching with Dependent Types}}, YEAR = {1992}, crossref = {Bastad92} @@ -289,7 +284,6 @@ s}, @INPROCEEDINGS{Coquand93, AUTHOR = {Th. Coquand}, - BOOKTITLE = {in \cite{Nijmegen93}}, TITLE = {{Infinite Objects in Type Theory}}, YEAR = {1993}, crossref = {Nijmegen93} @@ -308,7 +302,8 @@ s}, title = "Information Retrieval in a Coq Proof Library using Type Isomorphisms", booktitle = {Proceedings of TYPES'99, L\"okeberg}, - publisher = "Springer-Verlag LNCS", + publisher = SV, + series = lncs, year = "1999", url = "\\{\sf ftp://ftp.inria.fr/INRIA/Projects/coq/David.Delahaye/papers/}"# @@ -320,7 +315,8 @@ s}, title = "A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}", booktitle = "Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island", - publisher = "Springer-Verlag LNCS/LNAI", + publisher = SV, + series = LNCS, volume = "1955", pages = "85--95", month = "November", @@ -332,8 +328,8 @@ s}, @INPROCEEDINGS{DelMay01, author = "Delahaye, D. and Mayero, M.", - title = "{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels - en {{\sf Coq}}", + title = {{\tt Field}: une proc\'edure de d\'ecision pour les nombres r\'eels + en {\Coq}}, booktitle = "Journ\'ees Francophones des Langages Applicatifs, Pontarlier", publisher = "INRIA", month = "Janvier", @@ -347,18 +343,18 @@ s}, AUTHOR = {G. Dowek}, INSTITUTION = {INRIA}, NUMBER = {1283}, - TITLE = {{Naming and Scoping in a Mathematical Vernacular}}, + TITLE = {Naming and Scoping in a Mathematical Vernacular}, TYPE = {Research Report}, YEAR = {1990} } @ARTICLE{Dow91a, AUTHOR = {G. Dowek}, - JOURNAL = {{Compte Rendu de l'Acad\'emie des Sciences}}, - NOTE = {(The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors)}, + JOURNAL = {Compte-Rendus de l'Acad\'emie des Sciences}, + NOTE = {The undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors}, NUMBER = {12}, PAGES = {951--956}, - TITLE = {{L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}}, + TITLE = {L'Ind\'ecidabilit\'e du Filtrage du Troisi\`eme Ordre dans les Calculs avec Types D\'ependants ou Constructeurs de Types}, VOLUME = {I, 312}, YEAR = {1991} } @@ -368,9 +364,9 @@ s}, BOOKTITLE = {Proceedings of Mathematical Foundation of Computer Science}, NOTE = {Also INRIA Research Report}, PAGES = {151--160}, - PUBLISHER = {Springer-Verlag}, - SERIES = {LNCS}, - TITLE = {{A Second Order Pattern Matching Algorithm in the Cube of Typed {$\lambda$}-calculi}}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {A Second Order Pattern Matching Algorithm in the Cube of Typed $\lambda$-calculi}, VOLUME = {520}, YEAR = {1991} } @@ -378,18 +374,22 @@ s}, @PHDTHESIS{Dow91c, AUTHOR = {G. Dowek}, MONTH = dec, - SCHOOL = {{Universit\'e Paris 7}}, - TITLE = {{D\'emonstration automatique dans le Calcul des Constructions}}, + SCHOOL = {Universit\'e Paris 7}, + TITLE = {D\'emonstration automatique dans le Calcul des Constructions}, YEAR = {1991} } -@UNPUBLISHED{Dow92a, +@article{Dow92a, AUTHOR = {G. Dowek}, - NOTE = {To appear in Theoretical Computer Science}, - TITLE = {{The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}}, - YEAR = {1992} + TITLE = {The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable}, + YEAR = 1993, + journal = tcs, + volume = 107, + number = 2, + pages = {349-356} } + @ARTICLE{Dow94a, AUTHOR = {G. Dowek}, JOURNAL = {Annals of Pure and Applied Logic}, @@ -402,7 +402,7 @@ s}, @INPROCEEDINGS{Dow94b, AUTHOR = {G. Dowek}, BOOKTITLE = {Proceedings of the second international conference on typed lambda calculus and applications}, - TITLE = {{Lambda-calculus, Combinators and the Comprehension Schema}}, + TITLE = {Lambda-calculus, Combinators and the Comprehension Schema}, YEAR = {1995} } @@ -412,7 +412,8 @@ s}, EDITOR = {G. Huet and G. Plotkin}, PAGES = {59--79}, PUBLISHER = {Cambridge University Press}, - TITLE = {{Inductive sets and families in {Martin-L{\"o}f's Type Theory} and their set-theoretic semantics : An inversion principle for {Martin-L\"of's} type theory}}, + TITLE = {Inductive sets and families in {Martin-L{\"o}f's} + Type Theory and their set-theoretic semantics: An inversion principle for {Martin-L\"of's} type theory}, VOLUME = {14}, YEAR = {1991} } @@ -431,33 +432,39 @@ s}, AUTHOR = {J.-C. Filli\^atre}, MONTH = sep, SCHOOL = {DEA d'Informatique, ENS Lyon}, - TITLE = {Une proc\'edure de d\'ecision pour le {C}alcul des {P}r\'edicats {D}irect. {E}tude et impl\'ementation dans le syst\`eme {C}oq}, + TITLE = {Une proc\'edure de d\'ecision pour le Calcul des Pr\'edicats Direct. {\'E}tude et impl\'ementation dans le syst\`eme {\Coq}}, YEAR = {1994} } @TECHREPORT{Filliatre95, AUTHOR = {J.-C. Filli\^atre}, INSTITUTION = {LIP-ENS-Lyon}, - TITLE = {{A decision procedure for Direct Predicate Calculus}}, + TITLE = {A decision procedure for Direct Predicate Calculus}, TYPE = {Research report}, NUMBER = {96--25}, YEAR = {1995} } -@Unpublished{Filliatre00a, - author = {J.-C. Filli\^atre}, - title = {{Verification of Non-Functional Programs - using Interpretations in Type Theory}}, - month = {February}, - year = 2000, - note = {To appear in the Journal of Functional Programming. - [English translation of \cite{Filliatre99}]}, - url = {\url{http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}} +@Article{Filliatre03jfp, + author = {J.-C. Filli{\^a}tre}, + title = {Verification of Non-Functional Programs + using Interpretations in Type Theory}, + journal = jfp, + volume = 13, + number = 4, + pages = {709--745}, + month = jul, + year = 2003, + note = {[English translation of \cite{Filliatre99}]}, + url = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz}, + topics = "team, lri", + type_publi = "irevcomlec" } + @PhdThesis{Filliatre99, author = {J.-C. Filli\^atre}, - title = {{Preuve de programmes imp\'eratifs en th\'eorie des types}}, + title = {Preuve de programmes imp\'eratifs en th\'eorie des types}, type = {Th{\`e}se de Doctorat}, school = {Universit\'e Paris-Sud}, year = 1999, @@ -476,7 +483,7 @@ s}, @InProceedings{FilliatreMagaud99, author = {J.-C. Filli\^atre and N. Magaud}, - title = {{Certification of sorting algorithms in the system Coq}}, + title = {Certification of sorting algorithms in the system {\Coq}}, booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends}, year = 1999, @@ -503,9 +510,9 @@ s}, AUTHOR = {E. Gim\'enez}, BOOKTITLE = {Types'94 : Types for Proofs and Programs}, NOTE = {Extended version in LIP research report 95-07, ENS Lyon}, - PUBLISHER = {Springer-Verlag}, - SERIES = {LNCS}, - TITLE = {{Codifying guarded definitions with recursive schemes}}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {Codifying guarded definitions with recursive schemes}, VOLUME = {996}, YEAR = {1994} } @@ -521,13 +528,13 @@ s}, @INPROCEEDINGS{Gimenez95b, AUTHOR = {E. Gim\'enez}, BOOKTITLE = {Workshop on Types for Proofs and Programs}, - SERIES = {LNCS}, + SERIES = LNCS, NUMBER = {1158}, PAGES = {135-152}, TITLE = {An application of co-Inductive types in Coq: verification of the Alternating Bit Protocol}, EDITORS = {S. Berardi and M. Coppo}, - PUBLISHER = {Springer-Verlag}, + PUBLISHER = SV, YEAR = {1995} } @@ -570,7 +577,7 @@ s}, AUTHOR = {D. Hirschkoff}, MONTH = sep, SCHOOL = {DEA IARFA, Ecole des Ponts et Chauss\'ees, Paris}, - TITLE = {{Ecriture d'une tactique arithm\'etique pour le syst\`eme Coq}}, + TITLE = {{\'E}criture d'une tactique arithm\'etique pour le syst\`eme {\Coq}}, YEAR = {1994} } @@ -594,16 +601,29 @@ s}, +@InProceedings{Hue87tapsoft, + author = {G. Huet}, + title = {Programming of Future Generation Computers}, + booktitle = {Proceedings of TAPSOFT87}, + series = LNCS, + volume = 249, + pages = {276--286}, + year = 1987, + publisher = SV +} + @INPROCEEDINGS{Hue87, AUTHOR = {G. Huet}, BOOKTITLE = {Programming of Future Generation Computers}, EDITOR = {K. Fuchi and M. Nivat}, - NOTE = {Also in Proceedings of TAPSOFT87, LNCS 249, Springer-Verlag, 1987, pp 276--286}, + NOTE = {Also in \cite{Hue87tapsoft}}, PUBLISHER = {Elsevier Science}, TITLE = {Induction Principles Formalized in the {Calculus of Constructions}}, YEAR = {1988} } + + @INPROCEEDINGS{Hue88, AUTHOR = {G. Huet}, BOOKTITLE = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, @@ -626,9 +646,9 @@ s}, AUTHOR = {G. Huet}, BOOKTITLE = {Proceedings of 12th FST/TCS Conference, New Delhi}, PAGES = {229--240}, - PUBLISHER = {Springer Verlag}, - SERIES = {LNCS}, - TITLE = {{The Gallina Specification Language : A case study}}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {The Gallina Specification Language : A case study}, VOLUME = {652}, YEAR = {1992} } @@ -718,7 +738,7 @@ Matching and Term Rewriting}, AUTHOR = {F. Leclerc and C. Paulin-Mohring}, BOOKTITLE = {{Types for Proofs and Programs, Types' 93}}, EDITOR = {H. Barendregt and T. Nipkow}, - PUBLISHER = {Springer-Verlag}, + PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{Programming with Streams in Coq. A case study : The Sieve of Eratosthenes}}, VOLUME = {806}, @@ -782,7 +802,7 @@ of the {ML} language}, EDITOR = {M. Bezem and J.-F. Groote}, NOTE = {Also LIP research report 92-49, ENS Lyon}, NUMBER = {664}, - PUBLISHER = {Springer-Verlag}, + PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{Inductive Definitions in the System Coq - Rules and Properties}}, YEAR = {1993} @@ -815,15 +835,6 @@ of the {ML} language}, Type = {Th\`ese de Doctorat} } -@BOOK{Nijmegen93, - EDITOR = {H. Barendregt and T. Nipkow}, - PUBLISHER = {Springer-Verlag}, - SERIES = {LNCS}, - TITLE = {Types for Proofs and Programs}, - VOLUME = {806}, - YEAR = {1994} -} - @BOOK{NoPS90, AUTHOR = {B. {Nordstr\"om} and K. Peterson and J. Smith}, BOOKTITLE = {Information Processing 83}, @@ -855,7 +866,7 @@ of the {ML} language}, EDITOR = {A. Voronkov}, MONTH = jul, NUMBER = {624}, - PUBLISHER = {Springer-Verlag}, + PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{ProPre : A Programming language with proofs}}, YEAR = {1992} @@ -883,7 +894,7 @@ of the {ML} language}, @INPROCEEDINGS{Parent95b, AUTHOR = {C. Parent}, BOOKTITLE = {{Mathematics of Program Construction'95}}, - PUBLISHER = {Springer-Verlag}, + PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{Synthesizing proofs from programs in the Calculus of Inductive Constructions}}, @@ -894,7 +905,7 @@ the Calculus of Inductive Constructions}}, @INPROCEEDINGS{Prasad93, AUTHOR = {K.V. Prasad}, BOOKTITLE = {{Proceedings of CONCUR'93}}, - PUBLISHER = {Springer-Verlag}, + PUBLISHER = SV, SERIES = {LNCS}, TITLE = {{Programming with broadcasts}}, VOLUME = {715}, @@ -937,8 +948,8 @@ into Interactive Proof Assistants}, BOOKTITLE = {Proceedings of International Joint Conference on Automated Reasoning}, EDITOR = {R. Gore and A. Leitsch and T. Nipkow}, - PUBLISHER = {Springer}, - SERIES = {LNAI}, + PUBLISHER = SV, + SERIES = LNAI, VOLUME = {2083}, PAGES = {421--426}, YEAR = {2001} @@ -1020,7 +1031,7 @@ Recursive Functions as Typed $\lambda-$Terms}}, AUTHOR = {L.Puel and A. Su\'arez}, BOOKTITLE = {{Conference Lisp and Functional Programming}}, SERIES = {ACM}, - PUBLISHER = {Springer-Verlag}, + PUBLISHER = SV, TITLE = {{Compiling Pattern Matching by Term Decomposition}}, YEAR = {1990} @@ -1050,3 +1061,23 @@ Languages}, PUBLISHER = {Prentice-Hall}, YEAR = {1987} } + + +@COMMENT{cross-references, must be at end} + +@BOOK{Bastad92, + EDITOR = {B. Nordstr\"om and K. Petersson and G. Plotkin}, + PUBLISHER = {Available by ftp at site ftp.inria.fr}, + TITLE = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}, + YEAR = {1992} +} + +@BOOK{Nijmegen93, + EDITOR = {H. Barendregt and T. Nipkow}, + PUBLISHER = SV, + SERIES = LNCS, + TITLE = {Types for Proofs and Programs}, + VOLUME = {806}, + YEAR = {1994} +} + diff --git a/doc/headers.tex b/doc/headers.tex index cccd277c3..c10dca58e 100644 --- a/doc/headers.tex +++ b/doc/headers.tex @@ -23,7 +23,9 @@ \renewcommand{\contentsname}{% \protect\setheaders{Table of contents}Table of contents} \renewcommand{\bibname}{\protect\setheaders{Bibliography}% +%BEGIN LATEX \protect\RefManCutCommand{BEGINBIBLIO=\thepage}% +%ENDLATEX \protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |