Various clean-ups

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

1 files changed, 9 insertions, 2 deletions

diff --git a/doc/index.html b/doc/index.html
index f300af9..a5741f5 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -60,7 +60,7 @@ overview papers above were written.</P>
 <A HREF="http://compcert.inria.fr/">the Compcert Web site</A>.</P>
 
 <P>This document and the Compcert sources are
-copyright 2005, 2006, 2007, 2008 Institut National de Recherche en
+copyright 2005, 2006, 2007, 2008, 2009 Institut National de Recherche en
 Informatique et en Automatique (INRIA) and distributed under the terms
 of the following <A HREF="LICENSE">license</A>.
 </P>
@@ -119,7 +119,7 @@ code, control-flow graph, finitely many physical registers, infinitely
 many stack slots). <BR>
 See also: <A HREF="html/Locations.html">Locations</A> (representation of
 locations).
-<LI> <A HREF="html/LTL.html">LTLin</A>: like LTL, but the CFG is
+<LI> <A HREF="html/LTLin.html">LTLin</A>: like LTL, but the CFG is
 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.
@@ -172,6 +172,13 @@ code.
 </TR>
 
 <TR valign="top">
+  <TD>Recognition of tail calls</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/Tailcall.html">Tailcall</A></TD>
+  <TD><A HREF="html/Tailcallproof.html">Tailcallproof</A></TD>
+</TR>
+
+<TR valign="top">
   <TD>Constant propagation</TD>
   <TD>RTL to RTL</TD>
   <TD><A HREF="html/Constprop.html">Constprop</A></TD>