diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-31 17:08:46 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-31 17:08:46 +0000 |
commit | 108804d88e16b00f171c2ac546c6c1a60f3c3ff8 (patch) | |
tree | aa2e19bcd7b8f349d7c4b557cc452bb3be55f2ec | |
parent | 636e45004c6fc3530f47ae237802bec732c32b30 (diff) | |
download | compcert-108804d88e16b00f171c2ac546c6c1a60f3c3ff8.tar.gz compcert-108804d88e16b00f171c2ac546c6c1a60f3c3ff8.zip |
Simplification des Cconst_symbol: seules les versions 'signed' sont conservees
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@443 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | extraction/extraction.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index e0f965d7..22df5933 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -51,10 +51,8 @@ Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". (* PPC *) -Extract Constant PPC.low_half_signed => "fun _ -> assert false". -Extract Constant PPC.high_half_signed => "fun _ -> assert false". -Extract Constant PPC.low_half_unsigned => "fun _ -> assert false". -Extract Constant PPC.high_half_unsigned => "fun _ -> assert false". +Extract Constant PPC.low_half => "fun _ -> assert false". +Extract Constant PPC.high_half => "fun _ -> assert false". (* Suppression of stupidly big equality functions *) Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y". |