aboutsummaryrefslogtreecommitdiffstats
path: root/doc/index.html
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-08-23 11:45:14 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-08-23 11:45:14 +0000
commitca0117ca268873766ac4fda3771295842b17fcd6 (patch)
treea4558d7703fede5c4045748a2e9fed11173cdcac /doc/index.html
parent8c697ac826f8bcac956fe8a6c6356a6c459d3c92 (diff)
downloadcompcert-kvx-ca0117ca268873766ac4fda3771295842b17fcd6.tar.gz
compcert-kvx-ca0117ca268873766ac4fda3771295842b17fcd6.zip
Doc fixes
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1726 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc/index.html')
-rw-r--r--doc/index.html3
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/index.html b/doc/index.html
index 84d2905d..1fd7859a 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -112,7 +112,8 @@ semantics.
<LI> The Compcert C source language:
<A HREF="html/Csyntax.html">syntax</A> and
<A HREF="html/Csem.html">semantics</A> and
-<A HREF="html/Cstrategy.html">determinized semantics</A>.
+<A HREF="html/Cstrategy.html">determinized semantics</A>.<BR>
+See also: <A HREF="html/Cexec.html">reference interpreter</A>.
<LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of Cmedium where expressions contain no side-effects.
<LI> <A HREF="html/Csharpminor.html">Csharpminor</A>: low-level
structured language.