aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTLmatchRTL.v
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling/BTLmatchRTL.v')
-rw-r--r--scheduling/BTLmatchRTL.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v
index 439ba9cc..a59c847e 100644
--- a/scheduling/BTLmatchRTL.v
+++ b/scheduling/BTLmatchRTL.v
@@ -412,7 +412,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
else Error (msg "BTL.verify_block: different r in Bload")
else Error (msg "BTL.verify_block: different lr in Bload")
else Error (msg "BTL.verify_block: different addressing in Bload")
- else Error (msg "BTL.verify_block: different mchunk in Bload")
+ else Error (msg "BTL.verify_block: different chunk in Bload")
else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload")
| _ => Error (msg "BTL.verify_block: incorrect cfg Bload")
end
@@ -426,7 +426,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
else Error (msg "BTL.verify_block: different r in Bstore")
else Error (msg "BTL.verify_block: different lr in Bstore")
else Error (msg "BTL.verify_block: different addressing in Bstore")
- else Error (msg "BTL.verify_block: different mchunk in Bstore")
+ else Error (msg "BTL.verify_block: different chunk in Bstore")
| _ => Error (msg "BTL.verify_block: incorrect cfg Bstore")
end
| Bseq b1 b2 =>