diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v index df1e050e776701a2dddcae8ad114d7d9f96ec9cd..f65b310ce07b3f2cb0a2e4b742db58dcf83d8eda 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).