From ba3fae4a579a49d594754f70db94931b201c4746 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 6 May 2020 23:54:27 +0200
Subject: [PATCH] Clean up
---
theories/examples/subprotocols.v | 5 +----
1 file changed, 1 insertion(+), 4 deletions(-)
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index 3ea323e..75f1d6d 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -7,9 +7,6 @@ Section basics.
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'.
- iSplitL; eauto with iFrame.
- Qed.
+ Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame. Qed.
End pair.
--
GitLab