aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Selection.v
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-01-01 12:47:42 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-01-01 12:47:42 +0000
commit2245717b5800da80371952999bc0cff5f75aa490 (patch)
tree607052bd5604bdd13e33530bcfa0f6f9e4b25e70 /arm/Selection.v
parent58fca75f4ab089d21fc4f4a5bdac71d4b79f899f (diff)
downloadcompcert-2245717b5800da80371952999bc0cff5f75aa490.tar.gz
compcert-2245717b5800da80371952999bc0cff5f75aa490.zip
Continuation of ARM port.
Cleaned up Makefile and SVN properties. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@935 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Selection.v')
-rw-r--r--arm/Selection.v3
1 files changed, 2 insertions, 1 deletions
diff --git a/arm/Selection.v b/arm/Selection.v
index d5eb6b8b..1b5411b1 100644
--- a/arm/Selection.v
+++ b/arm/Selection.v
@@ -1390,5 +1390,6 @@ Definition sel_fundef (f: Cminor.fundef) : fundef :=
Definition sel_program (p: Cminor.program) : program :=
transform_program sel_fundef p.
+(** For compatibility with PowerPC *)
-
+Parameter use_fused_mul: unit -> bool.