From fb202a70ccc2872aa3849854c09810a6bee268e5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 8 May 2011 08:39:30 +0000 Subject: powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination). Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- extraction/extraction.v | 1 + 1 file changed, 1 insertion(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 5fc6795..765bebd 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -91,6 +91,7 @@ Extract Constant Compiler.print_RTL_castopt => "PrintRTL.print_castopt". Extract Constant Compiler.print_RTL_constprop => "PrintRTL.print_constprop". Extract Constant Compiler.print_RTL_cse => "PrintRTL.print_cse". Extract Constant Compiler.print_LTLin => "PrintLTLin.print_if". +Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) -- cgit v1.2.3