diff --git a/doc/coq2html.css b/doc/coq2html.css
index 5a326a359f8fe9580913684905ac7295bc651b31..0f6680e8d0f632275ba0453a60bde1ffd3e2eca5 100644
--- a/doc/coq2html.css
+++ b/doc/coq2html.css
@@ -55,6 +55,10 @@ div.toggleproof {
   text-decoration: underline;
 }
 
+div.toggleproof:hover {
+  cursor: pointer;
+}
+
 div.proofscript {
   font-size: 0.8em;
 }
diff --git a/doc/index.html b/doc/index.html
index 3c7337b7fa9e537dd492bc3bf10546feb8f3d48c..dff66ce6b921fed7a32b4c1e1936adec95ae35cd 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.6, 2010-01-12</H3>
+<H3 align="center">Version 1.7, 2010-03-31</H3>
 
 <H2>Introduction</H2>
 
@@ -91,7 +91,9 @@ inequations by fixpoint iteration.
 common elements of abstract syntaxes.
 <LI> <A HREF="html/Values.html">Values</A>: run-time values.
 <LI> <A HREF="html/Events.html">Events</A>: observable events and traces.
-<LI> <A HREF="html/Mem.html">Mem</A>: the memory model.
+<LI> <A HREF="html/Memtype.html">Memtype</A>: memory model (interface). <BR>
+See also: <A HREF="html/Memory.html">Memory</A> (implementation of the memory model). <BR>
+See also: <A HREF="html/Memdata.html">Memdata</A> (in-memory representation of data).
 <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.