From d36fe30f241473e1d32c47a80a058b6e763d4bbf Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com> Date: Tue, 30 Jan 2024 11:29:22 +0100 Subject: [PATCH] Aligned fork_chan tactic binders with protocols --- 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 df1e050..f65b310 100644 --- a/theories/channel/proofmode.v +++ b/theories/channel/proofmode.v @@ -492,8 +492,8 @@ Tactic Notation "wp_new_chan" constr(prot) "as" Tactic Notation "wp_fork_chan" constr(prot) "as" simple_intropattern(c1) constr(pat1) "and" simple_intropattern(c2) constr(pat2) := - wp_smart_apply (fork_chan_spec prot); [iIntros (c1); iIntros pat1| - iIntros (c2); iIntros pat2]. + wp_smart_apply (fork_chan_spec prot); [iIntros (c2); iIntros pat2| + iIntros (c1); iIntros pat1]. Tactic Notation "wp_fork_chan" constr(prot) := wp_smart_apply (fork_chan_spec prot). -- GitLab