From fe4792ae0988575639a449466e08e2ab9d48abd3 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 12 Oct 2020 14:59:39 +0200
Subject: [PATCH] Fixed errata in tactic error message
---
theories/channel/proofmode.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 52bf7ef..58701fb 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;
--
GitLab