From 93a33f710ed9a5eb045d8ee09b6142142b172f18 Mon Sep 17 00:00:00 2001
From: xleroy
Date: Wed, 9 Jan 2013 10:35:04 +0000
Subject: Update for release 1.12
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2097 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
doc/index.html | 11 ++++++++---
1 file changed, 8 insertions(+), 3 deletions(-)
(limited to 'doc')
diff --git a/doc/index.html b/doc/index.html
index 095f082..172e18e 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.11, 2012-07-13
+Version 1.12, 2013-01-11
Introduction
@@ -63,7 +63,7 @@ written.
the Compcert Web site.
This document and the Compcert sources are
-copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012 Institut
+copyright 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013 Institut
National de Recherche en Informatique et en Automatique (INRIA) and
distributed under the terms of the
following license.
@@ -120,7 +120,6 @@ See also: type expressions and
operators (syntax and semantics) and
reference interpreter.
Clight: a simpler version of CompCert C where expressions contain no side-effects.
-operators (syntax and semantics).
Csharpminor: low-level
structured language.
Cminor: low-level structured
@@ -165,6 +164,12 @@ code.
SimplExprspec
SimplExprproof |
+
+ Pulling non-adressable scalar local variables out of memory |
+ Clight to Clight |
+ SimplLocals |
+ SimplLocalsproof
+
Simplification of control structures;
explication of type-dependent computations |
--
cgit v1.2.3