diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 14:06:09 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 14:06:09 +0100 |
| commit | 15e49a91f1496dd41f92a78069fe0d553ec5932b (patch) | |
| tree | dd077890512c32977434c2c2b3c919fcd8f5a0ea /backend/PrintXTL.ml | |
| parent | b7410c39f2ac8ecef788eaeb78c27e8275616700 (diff) | |
| download | compcert-kvx-15e49a91f1496dd41f92a78069fe0d553ec5932b.tar.gz compcert-kvx-15e49a91f1496dd41f92a78069fe0d553ec5932b.zip | |
Remove open Locations.
Locations are only used in two functions and can be referenced
there directly.
Diffstat (limited to 'backend/PrintXTL.ml')
| -rw-r--r-- | backend/PrintXTL.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index 31273f97..cc1f7d49 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -17,7 +17,6 @@ open Camlcoq open Datatypes open Maps open AST -open !Locations open PrintAST open PrintOp open XTL @@ -36,15 +35,15 @@ let short_name_of_type = function | Tany64 -> 'd' let loc pp = function - | R r -> mreg pp r - | S(Local, ofs, ty) -> + | Locations.R r -> mreg pp r + | Locations.S(Locations.Local, ofs, ty) -> fprintf pp "L%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) - | S(Incoming, ofs, ty) -> + | Locations.S(Locations.Incoming, ofs, ty) -> fprintf pp "I%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) - | S(Outgoing, ofs, ty) -> + | Locations.S(Locations.Outgoing, ofs, ty) -> fprintf pp "O%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs) -let current_alloc = ref (None: (var -> loc) option) +let current_alloc = ref (None: (var -> Locations.loc) option) let current_liveness = ref (None: VSet.t PMap.t option) let reg pp r ty = |