diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-23 11:45:14 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-23 11:45:14 +0000 |
commit | ca0117ca268873766ac4fda3771295842b17fcd6 (patch) | |
tree | a4558d7703fede5c4045748a2e9fed11173cdcac /doc/index.html | |
parent | 8c697ac826f8bcac956fe8a6c6356a6c459d3c92 (diff) | |
download | compcert-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.html | 3 |
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. |