diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 14:05:18 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-06 14:05:18 +0100 |
| commit | b7410c39f2ac8ecef788eaeb78c27e8275616700 (patch) | |
| tree | 439ca9b8763b81ca084d059613939e5d7849501a /backend/PrintLTL.ml | |
| parent | a03dda71ff004c7a2b02654d96887609ef11d9fa (diff) | |
| download | compcert-kvx-b7410c39f2ac8ecef788eaeb78c27e8275616700.tar.gz compcert-kvx-b7410c39f2ac8ecef788eaeb78c27e8275616700.zip | |
Remove open Locations.
The Locations are only used in one function.
Diffstat (limited to 'backend/PrintLTL.ml')
| -rw-r--r-- | backend/PrintLTL.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index a0a08218..d0557073 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -17,7 +17,6 @@ open Camlcoq open Datatypes open Maps open AST -open !Locations open LTL open PrintAST open PrintOp @@ -34,17 +33,17 @@ let rec mregs pp = function let slot pp (sl, ofs, ty) = match sl with - | Local -> + | Locations.Local -> fprintf pp "local(%ld,%s)" (camlint_of_coqint ofs) (name_of_type ty) - | Incoming -> + | Locations.Incoming -> fprintf pp "incoming(%ld,%s)" (camlint_of_coqint ofs) (name_of_type ty) - | Outgoing -> + | Locations.Outgoing -> fprintf pp "outgoing(%ld,%s)" (camlint_of_coqint ofs) (name_of_type ty) let loc pp l = match l with - | R r -> mreg pp r - | S(sl, ofs, ty) -> slot pp (sl, ofs, ty) + | Locations.R r -> mreg pp r + | Locations.S(sl, ofs, ty) -> slot pp (sl, ofs, ty) let rec locs pp = function | [] -> () |