diff --git a/doc/index.html b/doc/index.html
index a5741f5978711b90289ceb9b33c648b8e42cec66..47c849edfb50f4ff26561461192f3f562b30ddd7 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }
 
 <H1 align="center">The Compcert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 1.3, 2008-08-11</H3>
+<H3 align="center">Version 1.4, 2009-04-21</H3>
 
 <H2>Introduction</H2>
 
@@ -36,10 +36,10 @@ correctness --- the fact that the generated assembly code is
 semantically equivalent to its source program --- was entirely proved
 within the Coq proof assistant.</P>
 
-<P>A high-level overview of the Compcert compiler and its proof of 
-correctness can be found in the following papers:</P>
+<P>High-level descriptions of the Compcert compiler and its proof of 
+correctness can be found in the following papers (in increasing order of technical details):</P>
 <UL>
-<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. Draft submitted for publication, July 2008.
+<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
 <LI>Xavier Leroy, <A
 HREF="http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf">Formal
 certification of a compiler back-end, or: programming a compiler with
@@ -48,6 +48,7 @@ a proof assistant</A>.  Proceedings of the POPL 2006 symposium.
 <A HREF="http://gallium.inria.fr/~xleroy/publi/cfront.pdf">Formal
 verification of a C compiler front-end</A>. 
 Proceedings of Formal Methods 2006, LNCS 4085.
+<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. arXiv:0902.2137 [cs]. Draft submitted for publication, July 2008.
 </UL>
 
 <P>This Web site gives a commented listing of the underlying Coq
@@ -127,7 +128,7 @@ spilling, reloading and enforcement of calling conventions.
 view of the activation record.  <BR>
 See also: <A HREF="html/Machabstr.html">Machabstr</A> abstract semantics for Mach. <BR>
 See also: <A HREF="html/Machconcr.html">Machconcr</A> concrete semantics for Mach.
-<LI> <A HREF="html/PPC.html">PPC</A>: abstract syntax for PowerPC assembly
+<LI> <A HREF="html/Asm.html">Asm</A>: abstract syntax for PowerPC assembly
 code.
 </UL>
 
@@ -238,15 +239,15 @@ code.
   <TD>Storing the activation records in memory</TD>
   <TD>Mach to Mach</TD>
   <TD>(none)
-  <TD><A HREF="html/PPCgenretaddr.html">PPCgenretaddr</A><BR>
+  <TD><A HREF="html/Asmgenretaddr.html">Asmgenretaddr</A><BR>
       <A HREF="html/Machabstr2concr.html">Machabstr2concr</A></TD>
 
 <TR valign="top">
-  <TD>Emission of PowerPC assembly</TD>
-  <TD>Mach to PPC</TD>
-  <TD><A HREF="html/PPCgen.html">PPCgen</A></TD>
-  <TD><A HREF="html/PPCgenproof1.html">PPCgenproof1</A><BR>
-      <A HREF="html/PPCgenproof.html">PPCgenproof</A></TD>
+  <TD>Emission of assembly code</TD>
+  <TD>Mach to Asm</TD>
+  <TD><A HREF="html/Asmgen.html">Asmgen</A></TD>
+  <TD><A HREF="html/Asmgenproof1.html">Asmgenproof1</A><BR>
+      <A HREF="html/Asmgenproof.html">Asmgenproof</A></TD>
 </TR>
 </TABLE>