From 9ce1b23f6361d8070490df1269a7bc53aa215efb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 21 Jul 2021 12:16:27 +0200 Subject: expansions btl proofs --- scheduling/BTLmatchRTL.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'scheduling/BTLmatchRTL.v') 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 => -- cgit