diff options
Diffstat (limited to 'backend/PrintMach.ml')
| -rw-r--r-- | backend/PrintMach.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index 70e65832..3481421b 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -16,12 +16,11 @@ open Printf open Camlcoq open Datatypes open AST -open Machregsaux open Mach open PrintAST let reg pp r = - match name_of_register r with + match Machregsnames.name_of_register r with | Some s -> fprintf pp "%s" s | None -> fprintf pp "<unknown reg>" |