From 85c15c6453ae31e4a536aafb6bb3fde60432ce31 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 6 May 2020 23:59:14 +0200
Subject: [PATCH] More clean up
---
theories/examples/subprotocols.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index 75f1d6d..0295aff 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -6,7 +6,7 @@ Section basics.
Lemma reference_example (l2' : loc) :
l2' ↦ #22 -∗
(<! (l1 l2 : loc)> MSG (#l1, #l2) {{ l1 ↦ #20 ∗ l2 ↦ #22 }}; END)%proto ⊑
- (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END)%proto.
- Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame. Qed.
+ (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END)%proto.
+ Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed.
End pair.
--
GitLab