From c15e489422b7f6924e82da8c105a6654643e5650 Mon Sep 17 00:00:00 2001
From: xleroy
Date: Mon, 12 Mar 2012 14:01:47 +0000
Subject: MAJ doc
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1850 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
doc/index.html | 16 +++++-----------
1 file changed, 5 insertions(+), 11 deletions(-)
(limited to 'doc')
diff --git a/doc/index.html b/doc/index.html
index 1fd7859..f767b2a 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -24,7 +24,7 @@ a:active {color : Red; text-decoration : underline; }
The Compcert verified compiler
Commented Coq development
-Version 1.9, 2011-08-22
+Version 1.10, 2012-03-13
Introduction
@@ -63,9 +63,10 @@ written.
the Compcert Web site.
This document and the Compcert sources are
-copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011 Institut National de Recherche en
-Informatique et en Automatique (INRIA) and distributed under the terms
-of the following license.
+copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012 Institut
+National de Recherche en Informatique et en Automatique (INRIA) and
+distributed under the terms of the
+following license.
Table of contents
@@ -215,13 +216,6 @@ code.
CSEproof |
-
- Elimination of redundant casts |
- RTL to RTL |
- CastOptim |
- CastOptimproof |
-
-
Register allocation by coloring of an interference graph |
RTL to LTL |
--
cgit v1.2.3