From 3436ed78de535f48cff1ac84394c020450be8976 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 30 Mar 2010 12:40:47 +0000
Subject: Update for 1.7

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1304 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 doc/coq2html.css | 4 ++++
 doc/index.html   | 6 ++++--
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/coq2html.css b/doc/coq2html.css
index 5a326a3..0f6680e 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 3c7337b..dff66ce 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.
-- 
cgit v1.2.3