aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblock.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Asmblock.v')
-rw-r--r--aarch64/Asmblock.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 3ad1d7f8..16f8e0c0 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -604,7 +604,7 @@ Definition exec_load_rd_a (chunk: memory_chunk) (transf: val -> val)
Next (rs#r <- (transf v)) m.
Definition exec_load_double (chunk: memory_chunk) (transf: val -> val)
- (a: addressing) (rd1 rd2: preg) (rs: regset) (m: mem) :=
+ (a: addressing) (rd1 rd2: dreg) (rs: regset) (m: mem) :=
if is_pair_addressing_mode_correct a then
let addr := (eval_addressing a rs) in
let ofs := match chunk with | Mint32 => 4 | _ => 8 end in