Updates in preparation for release 2.00

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

1 files changed, 4 insertions, 5 deletions

diff --git a/Changelog b/Changelog
index c97fb1c..65e8e50 100644
--- a/Changelog
+++ b/Changelog
@@ -1,4 +1,4 @@
-Release 2.00, 2013-06-XX
+Release 2.00, 2013-06-21
 ========================
 
 Major improvements:
@@ -20,8 +20,7 @@ Major improvements:
   . two-address operations are treated more efficiently
   . no need to reserve processor registers for spilling and reloading.
   The improvements in quality of generated code is significant for
-  IA32 (because of its paucity of registers) and barely noticeable
-  for ARM and PowerPC.
+  IA32 (because of its paucity of registers) but less so for ARM and PowerPC.
 
 - Preliminary support for debugging information.  The "-g" flag
   causes DWARF debugging information to be generated for line numbers
@@ -49,7 +48,7 @@ Improvements in compiler usability:
 - Reduced memory requirements of constant propagation pass by forgetting
   compile-time approximations of dead variables.
 - More careful elaboration of C struct and union types into CompCert C
-  types, avoiding behaviors exponential in the nesting of structs.	 
+  types, avoiding behaviors exponential in the nesting of structs.
 
 Bug fixing:
 - Fixed parsing of labeled statements inside "switch" constructs,
@@ -61,7 +60,7 @@ Bug fixing:
 Coq development:
 - Adapted the memory model to the needs of the VST project at Princeton:
   . Memory block identifiers are now of type "positive" instead of "Z"
-  . Strengthened preconditions in the definition of memory injections
+  . Strengthened invariants in the definition of memory injections
     and the specification of external calls.
 - The LTL intermediate language is now a CFG of basic blocks.
 - Suppressed the LTLin intermediate language, no longer used.