From fab8ab30cc867ac860149b535394c252229957e6 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Mon, 8 Jul 2019 19:38:29 +0200 Subject: [PATCH] Fix typo. --- theories/channel/proofmode.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v index fc69165..aa99420 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'" -- GitLab