diff --git a/Changelog b/Changelog
index 8e253ee3acf17d58e6f784148ba2032b860e18fb..083940c9d61a4a15d556b0fe2e1da95c4e26339c 100644
--- a/Changelog
+++ b/Changelog
@@ -1,5 +1,5 @@
-Release 1.5
-=========
+Release 1.5, 2009-08-28
+=======================
- Support for "goto" in the source language Clight.
@@ -9,7 +9,7 @@ Release 1.5
tightened semantic preservation results accordingly.
- Fixed spurious compile-time error on Clight statements of the form
- "x = f(...)" where x is a global variable.
+ "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
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index e0d05f21953273e8e44b178b694ab2015fc6b677..ee13487582f42782f8b9108aca46f1ce65a5adbf 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -628,20 +628,20 @@ End EXPR.
Inductive cont: Type :=
| Kstop: cont
| Kseq: statement -> cont -> cont
- (* [Kseq s2 k] = after [s1] in [s1;s2] *)
+ (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
| Kwhile: expr -> statement -> cont -> cont
- (* [Kwhile e s k] = after [s] in [while (e) s] *)
+ (**r [Kwhile e s k] = after [s] in [while (e) s] *)
| Kdowhile: expr -> statement -> cont -> cont
- (* [Kdowhile e s k] = after [s] in [do s while (e)] *)
+ (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
| Kfor2: expr -> statement -> statement -> cont -> cont
- (* [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
+ (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
| Kfor3: expr -> statement -> statement -> cont -> cont
- (* [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
+ (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
| Kswitch: cont -> cont
- (* catches [break] statements arising out of [switch] *)
- | Kcall: option (block * int * type) -> (* where to store result *)
- function -> (* calling function *)
- env -> (* local env of calling function *)
+ (**r catches [break] statements arising out of [switch] *)
+ | Kcall: option (block * int * type) -> (**r where to store result *)
+ function -> (**r calling function *)
+ env -> (**r local env of calling function *)
cont -> cont.
(** Pop continuation until a call or stop *)
diff --git a/doc/index.html b/doc/index.html
index 47c849edfb50f4ff26561461192f3f562b30ddd7..88151d1bb0cf78b1dd1ae4261d55f3f238d389de 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 1.4, 2009-04-21</H3>
+<H3 align="center">Version 1.5, 2009-08-28</H3>
<H2>Introduction</H2>
@@ -83,9 +83,10 @@ semi-lattices.
<LI> <A HREF="html/Kildall.html">Kildall</A>: resolution of dataflow
inequations by fixpoint iteration.
<LI> <A HREF="html/Parmov.html">Parmov</A>: compilation of parallel assignments.
+<LI> <A HREF="html/UnionFind.html">UnionFind</A>: a persistent union-find data structure.
</UL>
-<H3>Definitions and properties used in many parts of the development</H3>
+<H3>Definitions and theorems used in many parts of the development</H3>
<UL>
<LI> <A HREF="html/Errors.html">Errors</A>: the Error monad.
@@ -96,6 +97,7 @@ common elements of abstract syntaxes.
<LI> <A HREF="html/Mem.html">Mem</A>: the memory model.
<LI> <A HREF="html/Globalenvs.html">Globalenvs</A>: global execution environments.
<LI> <A HREF="html/Smallstep.html">Smallstep</A>: tools for small-step semantics.
+<LI> <A HREF="html/Determinism.html">Determinism</A>: determinism properties of small-step semantics.
<LI> <A HREF="html/Op.html">Op</A>: operators, addressing modes and their
semantics.
</UL>
@@ -151,7 +153,9 @@ code.
<A HREF="html/Cshmgenproof2.html">Cshmgenproof2</A><br>
<A HREF="html/Cshmgenproof3.html">Cshmgenproof3</A></TD>
<TR valign="top">
- <TD>Stack allocation of local variables<br>whose address is taken</TD>
+ <TD>Stack allocation of local variables<br>
+ whose address is taken;<br>
+ simplification of switch statements</TD>
<TD>Csharpminor to Cminor</TD>
<TD><A HREF="html/Cminorgen.html">Cminorgen</A></TD>
<TD><A HREF="html/Cminorgenproof.html">Cminorgenproof</A></TD>
@@ -160,8 +164,10 @@ code.
<TR valign="top">
<TD>Recognition of operators<br>and addressing modes</TD>
<TD>Cminor to CminorSel</TD>
- <TD><A HREF="html/Selection.html">Selection</A></TD>
- <TD><A HREF="html/Selectionproof.html">Selectionproof</A></TD>
+ <TD><A HREF="html/Selection.html">Selection</A><br>
+ <A HREF="html/SelectOp.html">SelectOp</A></TD>
+ <TD><A HREF="html/Selectionproof.html">Selectionproof</A><br>
+ <A HREF="html/SelectOpproof.html">SelectOpproof</A></TD>
</TR>
<TR valign="top">
@@ -182,8 +188,10 @@ code.
<TR valign="top">
<TD>Constant propagation</TD>
<TD>RTL to RTL</TD>
- <TD><A HREF="html/Constprop.html">Constprop</A></TD>
- <TD><A HREF="html/Constpropproof.html">Constpropproof</A></TD>
+ <TD><A HREF="html/Constprop.html">Constprop</A><br>
+ <A HREF="html/ConstpropOp.html">ConstpropOp</A></TD>
+ <TD><A HREF="html/Constpropproof.html">Constpropproof</A><br>
+ <A HREF="html/ConstpropOpproof.html">ConstproppOproof</A></TD>
</TR>
<TR valign="top">
@@ -276,7 +284,7 @@ Proofs that compiler passes are type-preserving:
<H3>All together</H3>
<UL>
-<LI> <A HREF="html/Main.html">Main</A>: composing the passes together; the
+<LI> <A HREF="html/Compiler.html">Compiler</A>: composing the passes together; the
final semantic preservation theorems.
<LI> <A HREF="html/Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
</UL>