From 879ba4632717690cb3fbf0010b038fe6dc3c231e Mon Sep 17 00:00:00 2001
From: Xavier Leroy
Date: Sat, 13 Jan 2018 17:30:36 +0100
Subject: Preparations for release 3.2
---
Changelog | 7 +++++--
doc/index.html | 8 ++++----
2 files changed, 9 insertions(+), 6 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
diff --git a/doc/index.html b/doc/index.html
index d2a5b6cc..34583bd3 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 3.1, 2017-08-18
+Version 3.2, 2018-01-15
Introduction
@@ -39,8 +39,8 @@ within the Coq proof assistant.
High-level descriptions of the CompCert compiler and its proof of
correctness can be found in the following papers (in increasing order of technical details):
@@ -60,7 +60,7 @@ written.
This document and the CompCert sources are copyright Institut
National de Recherche en Informatique et en Automatique (INRIA) and
-distributed under the terms of the
+AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the
following license.
--
cgit