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