diff options
Diffstat (limited to 'arm/Selection.v')
| -rw-r--r-- | arm/Selection.v | 3 |
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. |