Updating doc for 1.13

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2142 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 5 insertions, 8 deletions

diff --git a/doc/index.html b/doc/index.html
index aa1847f..1f5d3ed 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.12, 2013-01-11</H3>
+<H3 align="center">Version 1.13, 2013-03-12</H3>
 
 <H2>Introduction</H2>
 
@@ -140,8 +140,7 @@ replaced by a linear list of instructions with explicit branches and labels.
 <LI> <A HREF="html/Linear.html">Linear</A>: like LTLin, with explicit
 spilling, reloading and enforcement of calling conventions.
 <LI> <A HREF="html/Mach.html">Mach</A>: like Linear, with a more concrete
-view of the activation record.  <BR>
-See also: <A HREF="html/Machsem.html">Machsem</A> operational semantics for Mach. <BR>
+view of the activation record.  
 <LI> <A HREF="html/Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly
 code.
 </UL>
@@ -298,15 +297,15 @@ code.
   <TD><A HREF="html/Stacking.html">Stacking</A><BR>
       <A HREF="html/Bounds.html">Bounds</A><BR>
       <A HREF="html/Stacklayout.html"><I>Stacklayout</I></A></TD>
-  <TD><A HREF="html/Stackingproof.html">Stackingproof</A><BR>
-      <A HREF="html/Asmgenretaddr.html"><I>Asmgenretaddr</I></A></TD>
+  <TD><A HREF="html/Stackingproof.html">Stackingproof</A></TD>
 </TR>
 
 <TR valign="top">
   <TD>Emission of assembly code</TD>
   <TD>Mach to Asm</TD>
   <TD><A HREF="html/Asmgen.html"><I>Asmgen</I></A></TD>
-  <TD><A HREF="html/Asmgenproof1.html"><I>Asmgenproof1</I></A><BR>
+  <TD><A HREF="html/Asmgenproof0.html"><I>Asmgenproof0</I></A><BR>
+      <A HREF="html/Asmgenproof1.html"><I>Asmgenproof1</I></A><BR>
       <A HREF="html/Asmgenproof.html"><I>Asmgenproof</I></A></TD>
 </TR>
 </TABLE>
@@ -321,7 +320,6 @@ reconstruction.
 <LI> <A HREF="html/LTLtyping.html">LTLtyping</A>: typing for LTL.
 <LI> <A HREF="html/LTLintyping.html">LTLintyping</A>: typing for LTLin.
 <LI> <A HREF="html/Lineartyping.html">Lineartyping</A>: typing for Linear.
-<LI> <A HREF="html/Machtyping.html">Machtyping</A>: typing for Mach.
 </UL>
 Proofs that compiler passes are type-preserving:
 <UL>
@@ -331,7 +329,6 @@ Proofs that compiler passes are type-preserving:
 <LI> <A HREF="html/CleanupLabelstyping.html">CleanupLabelstyping</A> (removal of unreferenced labels).
 <LI> <A HREF="html/Reloadtyping.html">Reloadtyping</A> (spilling and reloading).
 <LI> <A HREF="html/RREtyping.html">RREtyping</A> (redundant reload elimination).
-<LI> <A HREF="html/Stackingtyping.html">Stackingtyping</A> (layout of activation records).
 </UL>
 
 <H3>All together</H3>