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
---
Changelog | 2 +-
common/Globalenvs.v | 1 +
doc/index.html | 16 +++++-----------
3 files changed, 7 insertions(+), 12 deletions(-)
diff --git a/Changelog b/Changelog
index d660b651..d1e7e4c4 100644
--- a/Changelog
+++ b/Changelog
@@ -1,4 +1,4 @@
-Release 1.10, 2012-02-29
+Release 1.10, 2012-03-13
========================
Improvements in confidence:
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index e01d5f73..539bb77c 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -293,6 +293,7 @@ Qed.
Remark add_functions_inversion : forall fs e x b,
find_symbol (add_functions e fs) x = Some b ->
In x (funct_names fs) \/ find_symbol e x = Some b.
+Proof.
induction fs; intros.
simpl in H. intuition.
simpl in H. destruct (IHfs _ _ _ H).
diff --git a/doc/index.html b/doc/index.html
index 1fd7859a..f767b2a0 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