diff --git a/Changelog b/Changelog
index 004d5cbec4260efa27f1569607064bf4fb15a4f1..8e253ee3acf17d58e6f784148ba2032b860e18fb 100644
--- a/Changelog
+++ b/Changelog
@@ -1,3 +1,34 @@
+Release 1.5
+=========
+
+- Support for "goto" in the source language Clight.
+
+- Added small-step semantics for Clight.
+
+- Traces for diverging executions are now uniquely defined;
+  tightened semantic preservation results accordingly.
+
+- Fixed spurious compile-time error on Clight statements of the form
+  "x = f(...)" where x is a global variable.
+
+- Fixed spurious compile-time error on Clight initializers where
+  the initial value is the result of a floating-point computation
+  (e.g. "double x = 3.14159 / 2;").
+
+- Simplified the interface of the generic dataflow solver.
+
+- Reduced running time and memory requirements for the constant propagation
+  pass.
+
+- Improved the implementation of George and Appel's graph coloring heuristic:
+  runs faster, produces better results.
+
+- Revised the implementation of branch tunneling.
+
+- Improved modularization between processor-dependent and
+  processor-independent parts.
+
+
 Release 1.4.1, 2009-06-05
 =========================
 
diff --git a/README b/README
index 3b136a98a27d265d1804e3a30c8131247ca94283..42f0443c704feb36eeb1fc3c4c46a0058d85c383 100644
--- a/README
+++ b/README
@@ -46,7 +46,7 @@ PREREQUISITES:
   the search path.  For MacOS X, you can get them by installing the
   XCode development tools, as found on the installation DVDs.
 
-* The Coq proof assistant, version 8.1pl3.
+* The Coq proof assistant, version 8.2-1 or later.
   Coq is free software, available from http://coq.inria.fr/
 
 * The Caml functional language, version 3.10 or later.
@@ -121,7 +121,7 @@ The generated assembly code is left in file src1.s
 The subset of the C language accepted by Compcert is quite large.
 The main features of C that are not supported are:
   - The "long long" and "long double" types.
-  - The "goto" statement, and non-structured forms of the "switch" statement.
+  - Non-structured forms of the "switch" statement (Duff's device).
   - Variable-argument functions.
 The "ccomp" command will issue errors and diagnostics if it encounters
 a C construct that it cannot process.