presentation, biblio;

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8381 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 131 insertions, 83 deletions

diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex
index d467b84e61..3ddf2e0c5f 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 a5e3781997..98c5c4568b 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 3e1e14f81a..aac7fbda8f 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 9f66c2850b..223585d54c 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 02b82985d5..5fa42d5717 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 88cbbc57d2..1b75c92a35 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 4b47c50289..36a10f6649 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 0c594cfab3..9a598b193a 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 4936191660..f272a04f6d 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 3e1d963445..242eebd4ef 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 cccd277c3d..c10dca58e9 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}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%