diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 52bf7eff8b8f452bc0ffae0a5db1fe6a7bc912db..58701fb4fe75286f990a7d56b976900a5118c676 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -241,8 +241,8 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_recv _ _ Hnew K))
       |fail 1 "wp_recv: cannot find 'recv' in" e];
     [solve_mapsto ()
-       |iSolveTC || fail 1 "wp_send: protocol not of the shape <?>"
-    |iSolveTC || fail 1 "wp_send: cannot convert to telescope"
+       |iSolveTC || fail 1 "wp_recv: protocol not of the shape <?>"
+    |iSolveTC || fail 1 "wp_recv: cannot convert to telescope"
     |iSolveTC
     |pm_reduce; simpl; tac_intros;
      tac Hnew;