aboutsummaryrefslogtreecommitdiffstats
path: root/Changelog
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2018-01-13 17:30:36 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2018-01-13 17:30:36 +0100
commit879ba4632717690cb3fbf0010b038fe6dc3c231e (patch)
treefd74b5f6937005fb1e60e8bc6eb0d08f68bf56fb /Changelog
parenta010a28c9ec8fcb0d1b906a8e389a9b6c139c9bc (diff)
downloadcompcert-kvx-879ba4632717690cb3fbf0010b038fe6dc3c231e.tar.gz
compcert-kvx-879ba4632717690cb3fbf0010b038fe6dc3c231e.zip
Preparations for release 3.2
Diffstat (limited to 'Changelog')
-rw-r--r--Changelog7
1 files changed, 5 insertions, 2 deletions
diff --git a/Changelog b/Changelog
index 9b471b9c..552122e0 100644
--- a/Changelog
+++ b/Changelog
@@ -1,5 +1,8 @@
+Release 3.2, 2018-01-15
+=======================
+
Code generation and optimization:
-- Inline static functions that are called only once.
+- Inline static functions that are called only once.
Can be turned off by setting the "noinline" attribute on the function.
- More consistent detection and elimination of divisions by 1.
- ARM in Thumb mode: simpler instruction sequence for branch through jump table.
@@ -20,7 +23,7 @@ Usability:
Bug fixing:
- Issue #P25: make sure sizeof(long double) = sizeof(double) in all contexts.
- Issue #211: wrong scoping for C99 declarations within a "for" statement.
-
+
Coq and Caml development:
- Pull request #191: Support Coq version 8.7.0 and 8.7.1 in addition
to Coq 8.6.1. Coq 8.6 (.0) is no longer supported owing to an