1 files changed, 4 insertions, 4 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index dc1faddd..4de1a9d0 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -836,10 +836,10 @@ Qed.
 
 Definition data_preg (r: preg) : bool :=
   match r with
-  | IR X16 => false
-  | IR X30 => false
-  | IR _ => true
-  | FR _ => true
+  | DR (IR' X16) => false
+  | DR (IR' X30) => false
+  | DR (IR' _) => true
+  | DR (FR' _) => true
   | CR _ => false
   (* | SP => true; subsumed by IR (iregsp) *)
   | PC => false