Update for 1.8.1 release

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1607 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 31 insertions, 5 deletions

diff --git a/Changelog b/Changelog
index cc154e2..bf4a65b 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,26 @@
+Release 1.8.1, 2011-03-14
+=========================
+
+- Adapted to Coq 8.3pl1.
+
+- Reduced compilation times through several algorithmic improvements
+  (contributed by A. Pilkiewicz).
+
+- In the various semantics, allow float-to-int conversions to fail
+  (if the float argument is outside the range of representable ints).
+
+- Initialization of global C variables made more robust and proved correct.
+
+- ABI conformance improved:
+     . the "char" type is now signed for x86, remains unsigned for PowerPC and ARM
+     . placement of bit-fields now follows SVR4 conventions (affects PowerPC)
+
+- Bug fixes in the C pre-simplifier:
+     . nontermination with some recursive struct types
+     . issues with zero-width bit fields
+     . elimination of struct assignments duplicating some volatile accesses
+
+
 Release 1.8, 2010-09-21
 =======================
 
diff --git a/README b/README
index dd81ae3..07dd15f 100644
--- a/README
+++ b/README
@@ -19,9 +19,9 @@ purposes.
 COPYRIGHT:
 
 The Compcert verified compiler is Copyright 2004, 2005, 2006, 2007,
-2008, 2009, 2010 Institut National de Recherche en Informatique et en
-Automatique (INRIA).  It is distributed under the conditions stated in
-file LICENSE.
+2008, 2009, 2010, 2011 Institut National de Recherche en Informatique
+et en Automatique (INRIA).  It is distributed under the conditions
+stated in file LICENSE.
 
 
 SUPPORTED PLATFORMS:
@@ -49,10 +49,13 @@ PREREQUISITES:
 
 * The "gcc", "as" and "make" tools must be installed and accessible in
   the search path.  For MacOS X, you can get them by installing the
-  XCode development tools, as found on the installation DVDs.
+  XCode development tools, as found on the installation DVDs
+  or on http://developer.apple.com/.  For Microsoft Windows,
+  install the Cygwin environment http://www.cygwin.com/.
 
-* The Coq proof assistant, version 8.2pl1 or 8.2pl2.
+* The Coq proof assistant, version 8.3pl1.
   Coq is free software, available from http://coq.inria.fr/
+  The original version 8.3 is not compatible, nor any of the 8.2 versions.
 
 * The Caml functional language, version 3.10 or later.
   Caml is free software, available from http://caml.inria.fr/