Preparations for release 3.2

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

doc/index.html

@@ -24,7 +24,7 @@
 
 <H1 align="center">The CompCert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 3.1, 2017-08-18</H3>
+<H3 align="center">Version 3.2, 2018-01-15</H3>
 
 <H2>Introduction</H2>
 
@@ -39,8 +39,8 @@ <H2>Introduction</H2>
 <P>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):</P>
 <UL>
-<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
-<LI>Xavier Leroy, <A HREF="http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. 
+<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
+<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. 
 Journal of Automated Reasoning 43(4):363-446, 2009.
 </UL>
 
@@ -60,7 +60,7 @@ <H2>Introduction</H2>
 
 <P>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 <A HREF="LICENSE">license</A>.
 </P>