aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-10 13:12:31 +0000
committerGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-12-10 13:12:31 +0000
commit265d773ab32168fc1ae675332ed6a0e6df18080b (patch)
tree7d4f7c875d8cb4dbbf3bd87fb2b8bf04764570f2
parente31e599f5cd5e539987c2741fece8bb9474dbbc6 (diff)
presentation, biblio;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--doc/AddRefMan-pre.tex2
-rw-r--r--doc/Correctness.tex2
-rw-r--r--doc/Makefile2
-rw-r--r--doc/RefMan-ext.tex2
-rw-r--r--doc/RefMan-ide.tex3
-rwxr-xr-xdoc/RefMan-lib.tex4
-rwxr-xr-xdoc/RefMan-pre.tex3
-rwxr-xr-xdoc/RefMan-uti.tex2
-rw-r--r--doc/Reference-Manual.tex7
-rwxr-xr-xdoc/biblio.bib185
-rw-r--r--doc/headers.tex2
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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-21 19:57:22 +0000