From c6d2ef0c5c896a82295c1fb8a717ea29ee3c0e4d Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Oct 2012 07:12:33 +0000 Subject: Make Clight independent of CompCert C. Common parts are factored out in cfrontend/Ctypes.v and cfrontend/Cop.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2060 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- doc/index.html | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/index.html b/doc/index.html index c6be1c2..095f082 100644 --- a/doc/index.html +++ b/doc/index.html @@ -116,8 +116,11 @@ semantics. syntax and semantics and determinized semantics.
-See also: reference interpreter. +See also: type expressions and +operators (syntax and semantics) and +reference interpreter.
  • Clight: a simpler version of CompCert C where expressions contain no side-effects. +operators (syntax and semantics).
  • Csharpminor: low-level structured language.
  • Cminor: low-level structured -- cgit v1.2.3