From e6186854053179ecacfa8a3bcce6f6f4646c8db4 Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Fri, 28 Jun 2019 13:51:13 +0200
Subject: [PATCH] Bumped loop sort
---
theories/examples/loop_sort.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/examples/loop_sort.v b/theories/examples/loop_sort.v
index 8bdfe71..c947380 100644
--- a/theories/examples/loop_sort.v
+++ b/theories/examples/loop_sort.v
@@ -37,10 +37,10 @@ Section loop_sort.
Proof.
iIntros (Ψ) "Hc HΨ". iLöb as "IH" forall (c Ψ).
wp_rec. rewrite {2}loop_sort_protocol_unfold.
- wp_apply (branch_spec with "Hc"); iIntros ([]) "/= Hc"; wp_if.
+ wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.
{ wp_apply (list_sort_service_spec with "Hc"); iIntros "Hc".
by wp_apply ("IH" with "Hc"). }
- wp_apply (branch_spec with "Hc"); iIntros ([]) "/= Hc"; wp_if.
+ wp_apply (branch_spec with "Hc"); iIntros ([]) "/= [Hc _]"; wp_if.
- wp_apply (start_chan_proto_spec N loop_sort_protocol); iIntros (d) "Hd".
{ wp_apply ("IH" with "Hd"); auto. }
wp_apply (send_proto_spec with "Hc"); simpl.
--
GitLab