diff -dur pvs-4.2.ORIG/doc/api/Makefile.in pvs-4.2/doc/api/Makefile.in
--- pvs-4.2.ORIG/doc/api/Makefile.in	2007-05-19 17:05:32.000000000 -0600
+++ pvs-4.2/doc/api/Makefile.in	2009-11-06 10:30:25.765410326 -0700
@@ -22,6 +22,10 @@
 
 pvs-api.pdf : ${sources} ${grammar-tables}
 	pdflatex $<
+	makeindex -c pvs-api.idx
+	bibtex pvs-api || echo
+	pdflatex $<
+	pdflatex $<
 
 .PHONY: clean
 clean :
diff -dur pvs-4.2.ORIG/doc/api/pvs-api.tex pvs-4.2/doc/api/pvs-api.tex
--- pvs-4.2.ORIG/doc/api/pvs-api.tex	2007-05-19 17:05:32.000000000 -0600
+++ pvs-4.2/doc/api/pvs-api.tex	2009-11-06 10:30:25.767409186 -0700
@@ -8,7 +8,7 @@
 \usepackage{makeidx}
 \usepackage{relsize}
 \usepackage{boxedminipage}
-\usepackage{fancyheadings}
+\usepackage{fancyhdr}
 %\usepackage{../../pvs}
 \usepackage{url}
 \usepackage{../makebnf}
@@ -5962,7 +5962,7 @@
 from the root to the given sequent, of the form \texttt{top.0.1.3}.
 
 \bibliographystyle{plain}
-\bibliography{../pvs,/homes/owre/pvs3.0/doc/pvs}
+\bibliography{../pvs}
 
 {\smaller
 \printindex
diff -dur pvs-4.2.ORIG/doc/datatypes/datatypes.tex pvs-4.2/doc/datatypes/datatypes.tex
--- pvs-4.2.ORIG/doc/datatypes/datatypes.tex	2007-05-19 17:03:30.000000000 -0600
+++ pvs-4.2/doc/datatypes/datatypes.tex	2009-11-06 10:30:25.769462544 -0700
@@ -2,7 +2,7 @@
 % Master File: datatypes.tex
 \documentclass[11pt,twoside]{book}
 \usepackage{relsize,url,makeidx,alltt}
-\usepackage{fancyheadings}
+\usepackage{fancyhdr}
 \usepackage[chapter]{tocbibind}
 \makeatletter
 \@ifundefined{pdfoutput}%
@@ -2805,5 +2805,5 @@
 
 
 \bibliographystyle{alpha}
-\bibliography{/homes/rushby/jmr,/homes/shankar/tex}
+\bibliography{../pvs}
 \end{document}
diff -dur pvs-4.2.ORIG/doc/datatypes/Makefile pvs-4.2/doc/datatypes/Makefile
--- pvs-4.2.ORIG/doc/datatypes/Makefile	2007-05-19 17:03:30.000000000 -0600
+++ pvs-4.2/doc/datatypes/Makefile	2009-11-06 10:30:25.770464299 -0700
@@ -17,6 +17,10 @@
 
 datatypes.pdf : ${sources}
 	pdflatex $<
+	makeindex -c datatypes.idx
+	bibtex datatypes || echo
+	pdflatex $<
+	pdflatex $<
 
 .PHONY: clean
 clean :
diff -dur pvs-4.2.ORIG/doc/interpretations/interpretations.tex pvs-4.2/doc/interpretations/interpretations.tex
--- pvs-4.2.ORIG/doc/interpretations/interpretations.tex	2007-05-19 18:57:36.000000000 -0600
+++ pvs-4.2/doc/interpretations/interpretations.tex	2009-11-06 10:30:25.772441992 -0700
@@ -1200,5 +1200,5 @@
 \newpage
 \bibliographystyle{alpha}
 \addcontentsline{toc}{chapter}{Bibliography}
-\bibliography{/homes/rushby/jmr,/homes/owre/tex/sam,/homes/shankar/tex}
+\bibliography{../pvs}
 \end{document}
diff -dur pvs-4.2.ORIG/doc/language/language.tex pvs-4.2/doc/language/language.tex
--- pvs-4.2.ORIG/doc/language/language.tex	2006-09-21 22:54:57.000000000 -0600
+++ pvs-4.2/doc/language/language.tex	2009-11-06 10:30:25.773456354 -0700
@@ -6,7 +6,7 @@
 \usepackage{makeidx}
 \usepackage{relsize}
 \usepackage{boxedminipage}
-\usepackage{fancyheadings}
+\usepackage{fancyhdr}
 %\usepackage{../../pvs}
 \usepackage{url}
 \usepackage{../makebnf}
diff -dur pvs-4.2.ORIG/doc/language/Makefile.in pvs-4.2/doc/language/Makefile.in
--- pvs-4.2.ORIG/doc/language/Makefile.in	2006-09-21 22:54:57.000000000 -0600
+++ pvs-4.2/doc/language/Makefile.in	2009-11-06 10:30:25.773456354 -0700
@@ -43,6 +43,10 @@
 
 language.pdf : ${sources} ${grammar-tables}
 	pdflatex $<
+	makeindex -c language.idx
+	bibtex language || echo
+	pdflatex $<
+	pdflatex $<
 
 .PHONY: clean
 clean :
diff -dur pvs-4.2.ORIG/doc/prover/Makefile.in pvs-4.2/doc/prover/Makefile.in
--- pvs-4.2.ORIG/doc/prover/Makefile.in	2002-07-05 13:50:53.000000000 -0600
+++ pvs-4.2/doc/prover/Makefile.in	2009-11-06 10:30:25.774457266 -0700
@@ -17,6 +17,10 @@
 
 prover.pdf : ${sources}
 	pdflatex $<
+	makeindex -c prover.idx
+	bibtex prover || echo
+	pdflatex $<
+	pdflatex $<
 
 .PHONY: clean
 clean :
diff -dur pvs-4.2.ORIG/doc/prover/prover.tex pvs-4.2/doc/prover/prover.tex
--- pvs-4.2.ORIG/doc/prover/prover.tex	2006-09-21 23:13:37.000000000 -0600
+++ pvs-4.2/doc/prover/prover.tex	2009-11-06 10:30:25.777429336 -0700
@@ -1,7 +1,7 @@
 % Document Type: LaTeX
 % Master File: prover.tex
 \documentclass[12pt,twoside]{book}
-\usepackage{relsize,alltt,makeidx,url,boxedminipage,fancyheadings,tabularx}
+\usepackage{relsize,alltt,makeidx,url,boxedminipage,fancyhdr,tabularx}
 %\usepackage{../../pvs}
 \usepackage{../makebnf}
 \usepackage[chapter]{tocbibind}
diff -dur pvs-4.2.ORIG/doc/semantics/Makefile pvs-4.2/doc/semantics/Makefile
--- pvs-4.2.ORIG/doc/semantics/Makefile	2007-05-19 17:28:21.000000000 -0600
+++ pvs-4.2/doc/semantics/Makefile	2009-11-06 10:30:25.779593316 -0700
@@ -17,6 +17,10 @@
 
 semantics.pdf : ${sources}
 	pdflatex $<
+	makeindex -c semantics.idx
+	bibtex semantics || echo
+	pdflatex $<
+	pdflatex $<
 
 .PHONY: clean
 clean :
diff -dur pvs-4.2.ORIG/doc/user-guide/Makefile.in pvs-4.2/doc/user-guide/Makefile.in
--- pvs-4.2.ORIG/doc/user-guide/Makefile.in	2002-08-01 00:35:38.000000000 -0600
+++ pvs-4.2/doc/user-guide/Makefile.in	2009-11-06 10:31:27.193544625 -0700
@@ -20,11 +20,16 @@
 user-guide.ps : user-guide.dvi
 	dvips -o $@ $<
 
-user-guide.pdf : ${sources} pvs-screen1.pdf
-	pdflatex $<
+user-guide.pdf : $(headers) $(sources) pvs-screen1.pdf \
+		 sum-nosub.tex sum-sub.tex sum-tccs.tex
+	pdflatex user-guide
+	bibtex user-guide || echo
+	makeindex -o user-guide.ind user-guide.idx
+	pdflatex user-guide
+	pdflatex user-guide
 
 sum-nosub.tex sum-sub.tex sum-tccs.tex : sum.pvs sum.el
-	@PVSPATH@/pvs -batch -q -l sum.el -f kill-process
+	$(pvs-path)/pvs -batch -q -l sum.el
 
 .PHONY: clean
 clean :
diff -dur pvs-4.2.ORIG/doc/user-guide/user-guide.tex pvs-4.2/doc/user-guide/user-guide.tex
--- pvs-4.2.ORIG/doc/user-guide/user-guide.tex	2006-09-21 17:52:37.000000000 -0600
+++ pvs-4.2/doc/user-guide/user-guide.tex	2009-11-06 10:30:25.780423733 -0700
@@ -7,7 +7,7 @@
 %\usepackage{showidx}	% use for index debugging
 \usepackage{relsize}
 \usepackage{boxedminipage}
-\usepackage{fancyheadings}
+\usepackage{fancyhdr}
 \usepackage{graphicx}
 \usepackage{../../pvs}
 \usepackage{url}