From 879ba4632717690cb3fbf0010b038fe6dc3c231e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Sat, 13 Jan 2018 17:30:36 +0100
Subject: Preparations for release 3.2

---
 doc/index.html | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc/index.html')

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; }
 
 <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 @@ within the Coq proof assistant.</P>
 <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 @@ written.</P>
 
 <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>
 
-- 
cgit