From edc00e0c90a5598f653add89f42a095d8ee1b629 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 May 2014 15:52:42 +0000 Subject: Assorted fixes to fix parsing issues and be more GCC-like: - Moved scanning of char constants and string literals entirely to Lexer - Parser: separate STRING_LITERAL from CONSTANT to be closer to ISO C99 grammar - pre_parser: adapted + "asm" takes string_literal, not CONSTANT - Revised errors "inline doesnt belong here" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2492 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 29e6863..0f23264 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -112,6 +112,8 @@ Extract Constant Cabs.cabsloc => byteno: int; ident : int; }". +Extract Constant Cabs.string => "String.t". +Extract Constant Cabs.char_code => "int64". (* Int31 *) Extract Inductive Int31.digits => "bool" [ "false" "true" ]. @@ -122,9 +124,6 @@ Extract Constant Int31.compare31 => "Camlcoq.Int31.compare". Extract Constant Int31.On => "0". Extract Constant Int31.In => "1". -(* String in Cabs *) -Extract Constant Cabs.string => "String.t". - (* Processor-specific extraction directives *) Load extractionMachdep. -- cgit v1.2.3