diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-18 12:52:54 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-02-18 12:52:54 +0100 |
| commit | 8677f50de8515bd83221e6a3d79b0f3d6dae4cbf (patch) | |
| tree | 6c4b3d7bd0519e4aa507c9b42bcbba2e0e1dc443 /ia32 | |
| parent | a3c0094508f9f4985de4509380dada5f5c85e115 (diff) | |
| download | compcert-kvx-8677f50de8515bd83221e6a3d79b0f3d6dae4cbf.tar.gz compcert-kvx-8677f50de8515bd83221e6a3d79b0f3d6dae4cbf.zip | |
Removed some style issues.
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/TargetPrinter.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 2a6be734..0a14bf24 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -75,8 +75,8 @@ module type SYSTEM = end (* Printer functions for cygwin *) -module Cygwin_System = - (struct +module Cygwin_System : SYSTEM = + struct let raw_symbol oc s = fprintf oc "_%s" s @@ -120,11 +120,11 @@ module Cygwin_System = fprintf oc " .local %a\n" symbol name; print_comm_decl oc name sz al - end:SYSTEM) + end (* Printer functions for ELF *) -module ELF_System = - (struct +module ELF_System : SYSTEM = + struct let raw_symbol oc s = fprintf oc "%s" s @@ -167,11 +167,11 @@ module ELF_System = fprintf oc " .local %a\n" symbol name; print_comm_decl oc name sz al - end:SYSTEM) + end (* Printer functions for MacOS *) -module MacOS_System = - (struct +module MacOS_System : SYSTEM = + struct let raw_symbol oc s = fprintf oc "_%s" s @@ -235,7 +235,7 @@ module MacOS_System = fprintf oc " .lcomm %a, %s, %d\n" symbol name (Z.to_string sz) (log2 al) - end:SYSTEM) + end module Target(System: SYSTEM):TARGET = |