Update for 1.7

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1304 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

doc/coq2html.css

@@ -55,6 +55,10 @@ div.toggleproof {
   text-decoration: underline;
 }
 
+div.toggleproof:hover {
+  cursor: pointer;
+}
+
 div.proofscript {
   font-size: 0.8em;
 }

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.