diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-13 08:56:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-13 08:56:59 +0000 |
| commit | 926bf226e89e0a4935da8815852af76c8d2b3cdf (patch) | |
| tree | 042278266691bb7b5f7b1318328b280e5b58cc7b /doc | |
| parent | 07140213aec08f00440a89b710a4f14c6816c524 (diff) | |
Late update for 1.11
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1977 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/index.html | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/index.html b/doc/index.html index 2abb967..c6be1c2 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.10, 2012-03-13</H3> +<H3 align="center">Version 1.11, 2012-07-13</H3> <H2>Introduction</H2> @@ -206,7 +206,7 @@ code. <TD>Function inlining</TD> <TD>RTL to RTL</TD> <TD><A HREF="html/Inlining.html">Inlining</A></TD> - <TD><A HREF="html/Inliningspec.html">Inliningspec</A> + <TD><A HREF="html/Inliningspec.html">Inliningspec</A><BR> <A HREF="html/Inliningproof.html">Inliningproof</A></TD> </TR> @@ -229,8 +229,10 @@ code. <TR valign="top"> <TD>Common subexpression elimination</TD> <TD>RTL to RTL</TD> - <TD><A HREF="html/CSE.html">CSE</A></TD> - <TD><A HREF="html/CSEproof.html">CSEproof</A></TD> + <TD><A HREF="html/CSE.html">CSE</A><BR> + <A HREF="html/CombineOp.html"><I>CombineOp</I></A></TD> + <TD><A HREF="html/CSEproof.html">CSEproof</A><BR> + <A HREF="html/CombineOpproof.html"><I>CombineOpproof</I></A></TD> </TR> <TR valign="top"> |