diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-11-29 14:44:01 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-11-29 14:44:01 +0100 |
| commit | d4070c456e71b6edfc9b65e5ec837370fea8e9d0 (patch) | |
| tree | bbbd904c1712af825aa5782eae0654ed1bdd9796 /arm/TargetPrinter.ml | |
| parent | 1d2538911835437edc88227aa648c69fe6eea456 (diff) | |
| download | compcert-kvx-d4070c456e71b6edfc9b65e5ec837370fea8e9d0.tar.gz compcert-kvx-d4070c456e71b6edfc9b65e5ec837370fea8e9d0.zip | |
Remove unused float_abi_type.
Diffstat (limited to 'arm/TargetPrinter.ml')
| -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 |