diff options
-rw-r--r-- | arm/TargetPrinter.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 57caed95..ebaaf50e 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -20,20 +20,13 @@ open Asm open PrintAsmaux open Fileinfo -(* Type for the ABI versions *) -type float_abi_type = - | Hard - | Soft - (* Module type for the options *) module type PRINTER_OPTIONS = sig - val float_abi: float_abi_type val vfpv3: bool val hardware_idiv: bool end - (* Basic printing functions *) let int_reg_name = function @@ -747,11 +740,6 @@ let sel_target () = let vfpv3 = Configuration.model >= "armv7" - let float_abi = match Configuration.abi with - | "eabi" -> Soft - | "hardfloat" -> Hard - | _ -> assert false - let hardware_idiv = match Configuration.model with | "armv7r" | "armv7m" -> !Clflags.option_mthumb |