diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 13:41:12 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 13:41:12 +0100 |
| commit | ca42ad21fe033f8ed31c168a0d1fd46a51eefc2c (patch) | |
| tree | 7e9eae0e2afa01429c354509ef1460e301161ceb /x86 | |
| parent | 53558488195a75ba06790972d3adfe44e8c4f4ee (diff) | |
| download | compcert-kvx-ca42ad21fe033f8ed31c168a0d1fd46a51eefc2c.tar.gz compcert-kvx-ca42ad21fe033f8ed31c168a0d1fd46a51eefc2c.zip | |
Inline open Datatypes.
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/TargetPrinter.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index b5aeefae..5fb8ae0c 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -13,7 +13,6 @@ (* Printing x86-64 assembly code in asm syntax *) open Printf -open !Datatypes open Camlcoq open Sections open AST @@ -244,9 +243,9 @@ module Target(System: SYSTEM):TARGET = let addressing_gen ireg oc (Addrmode(base, shift, cst)) = begin match cst with - | Coq_inl n -> + | Datatypes.Coq_inl n -> fprintf oc "%s" (Z.to_string n) - | Coq_inr(id, ofs) -> + | Datatypes.Coq_inr(id, ofs) -> if Archi.ptr64 then begin (* RIP-relative addressing *) let ofs' = Z.to_int64 ofs in |