From 7dd08351a9167f99c04f47042fb83c03e10d5552 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 11 Mar 2013 09:40:40 +0000
Subject: Updated for version 1.13

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2143 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 Changelog | 32 ++++++++++++++++++++++----------
 VERSION   |  3 ++-
 2 files changed, 24 insertions(+), 11 deletions(-)

diff --git a/Changelog b/Changelog
index 5bf73352..65a72369 100644
--- a/Changelog
+++ b/Changelog
@@ -1,24 +1,36 @@
-Development version
-===================
+Release 1.13, 2013-03-12
+========================
 
-- More efficient implementation of machine integers (module Integers)
-  taking advantage of bitwise operations defined in ZArith in Coq 8.4.
-- Fixed a bug in the reference interpreter in -all mode causing some
-  reductions to be incorrectly merged.
-- Better error and warning messages for declarations of variables
-  of size >= 2^32 bits.
+Language semantics:
 - Comparisons involving pointers "one past" the end of a block are
   now defined.  (They used to be undefined behavior.)
   (Contributed by Robbert Krebbers).
+
+Language features:
 - Arguments to __builtin_annot() that are compile-time constants
   are now replaced by their (integer or float) value in the annotation
   generated in the assembly file.
+
+Improvements in performance:
 - ARM and PowerPC ports: more efficient access to function parameters
   that are passed on the call stack.
 - ARM port; slightly better code generated for some indirect memory
   accesses.
-- Coq cleanups: a number of definitions that were opaque for no good reason
-  are now properly transparent.
+
+Improvements in usability:
+- Better error and warning messages for declarations of variables
+  of size >= 2^32 bits.
+- Fixed a bug in the reference interpreter in -all mode causing some
+  reductions to be incorrectly merged.
+- Reference interpreter: more efficient exploration of states in -all mode.
+
+Coq development:
+- More efficient implementation of machine integers (module Integers)
+  taking advantage of bitwise operations defined in ZArith in Coq 8.4.
+- Revised handling of return addresses in the Mach language
+  and the Stacking and Asmgen passes.
+- A number of definitions that were opaque for no good reason are now
+  properly transparent.
 
 
 Release 1.12.1, 2013-01-29
diff --git a/VERSION b/VERSION
index 4fedb2b6..fda763cb 100644
--- a/VERSION
+++ b/VERSION
@@ -1,2 +1,3 @@
-1.12
+1.13
+
 
-- 
cgit