From 926bf226e89e0a4935da8815852af76c8d2b3cdf Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 13 Jul 2012 08:56:59 +0000 Subject: Late update for 1.11 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1977 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'doc') 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; }

The Compcert verified compiler

Commented Coq development

-

Version 1.10, 2012-03-13

+

Version 1.11, 2012-07-13

Introduction

@@ -206,7 +206,7 @@ code. Function inlining RTL to RTL Inlining - Inliningspec + Inliningspec
Inliningproof @@ -229,8 +229,10 @@ code. Common subexpression elimination RTL to RTL - CSE - CSEproof + CSE
+ CombineOp + CSEproof
+ CombineOpproof -- cgit v1.2.3