From 82d24661bf10875afa1a56868ef87649623a4687 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 27 Aug 2009 09:47:59 +0000 Subject: Updated for release 1.5 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1141 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- README | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'README') diff --git a/README b/README index 3b136a9..42f0443 100644 --- a/README +++ b/README @@ -46,7 +46,7 @@ PREREQUISITES: the search path. For MacOS X, you can get them by installing the XCode development tools, as found on the installation DVDs. -* The Coq proof assistant, version 8.1pl3. +* The Coq proof assistant, version 8.2-1 or later. Coq is free software, available from http://coq.inria.fr/ * The Caml functional language, version 3.10 or later. @@ -121,7 +121,7 @@ The generated assembly code is left in file src1.s The subset of the C language accepted by Compcert is quite large. The main features of C that are not supported are: - The "long long" and "long double" types. - - The "goto" statement, and non-structured forms of the "switch" statement. + - Non-structured forms of the "switch" statement (Duff's device). - Variable-argument functions. The "ccomp" command will issue errors and diagnostics if it encounters a C construct that it cannot process. -- cgit v1.2.3