aboutsummaryrefslogtreecommitdiffstats
path: root/backend/PrintXTL.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2020-04-29 15:12:54 +0200
committerXavier Leroy <xavierleroy@users.noreply.github.com>2020-06-28 10:07:02 +0200
commitad2ea9c2e701dd82c26e6cd3e8a777be9bdef2a2 (patch)
tree128b7e26ed98c6035331adfd880103e89e25200b /backend/PrintXTL.ml
parentfaa1d7fbfd7c9d5aa333d9b353a6118e105c4428 (diff)
downloadcompcert-kvx-ad2ea9c2e701dd82c26e6cd3e8a777be9bdef2a2.tar.gz
compcert-kvx-ad2ea9c2e701dd82c26e6cd3e8a777be9bdef2a2.zip
Move shared code in new file.
The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file.
Diffstat (limited to 'backend/PrintXTL.ml')
-rw-r--r--backend/PrintXTL.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index 6432682a..aeaef25e 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -22,7 +22,7 @@ open PrintOp
open XTL
let mreg pp r =
- match Machregsaux.name_of_register r with
+ match Machregsnames.name_of_register r with
| Some s -> fprintf pp "%s" s
| None -> fprintf pp "<unknown machreg>"