diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v index fc69165a1bfaf4d26800e46548f87edccd4b5a2f..aa99420a3124792a2d5b5534d4a1965a55312208 100644 --- a/theories/channel/proofmode.v +++ b/theories/channel/proofmode.v @@ -140,7 +140,7 @@ Tactic Notation "wp_send_core" tactic3(tac_exist) "with" constr(pat) := | |- ∃ _, _ => eexists _ end; lazymatch goal with - | |- False => fail "wp_send:" Hs' "not fresh" + | |- False => fail "wp_send:" Hs' "not found" | _ => split; [try fast_done|split;[iFrame Hs_frame; solve_done d|wp_finish]] end] | _ => fail "wp_send: not a 'wp'"