From 8b6037d5d0790c9c2bc46629b7f0aab91812ef25 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 13 Nov 2023 12:07:13 +0100
Subject: [PATCH] Remove superfluous unfolds
---
gpfsl-examples/queue/proof_spsc_graph.v | 2 +-
gpfsl-examples/stack/proof_elim_graph.v | 2 +-
gpfsl-examples/stack/proof_treiber_history.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/gpfsl-examples/queue/proof_spsc_graph.v b/gpfsl-examples/queue/proof_spsc_graph.v
index 5541b28c..bc2de328 100644
--- a/gpfsl-examples/queue/proof_spsc_graph.v
+++ b/gpfsl-examples/queue/proof_spsc_graph.v
@@ -157,7 +157,7 @@ Proof.
iIntros (Φ) "_ Post".
iMod QE_alloc as (γed) "(â—ed & â—¯e & â—¯d)".
iApply (wq.(new_queue_spec) with "[%//]").
- iIntros "!> * [#QL QI]". iApply "Post". unfold SPSCInv.
+ iIntros "!> * [#QL QI]". iApply "Post".
iFrame "#∗". iPureIntro. split_and!; [done..|].
exists []. split_and!; [done|done|done| |done..].
split; [done|]. intros (?&?&?). done.
diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index 1f24d1d6..366cd6dc 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -749,7 +749,7 @@ Lemma StackInv'_graph_master_acc_instance :
∃ q', graph_master γg q' G ∗ (graph_master γg q' G -∗ StackInv' γg s q G).
Proof.
intros. iDestruct 1 as (?????????) "[(?&?&?) ?]".
- iExists _. iFrame. iIntros "?". unfold StackInv'. eauto 10 with iFrame.
+ iExists _. iFrame. by iIntros "?".
Qed.
Lemma StackInv'_graph_snap_instance :
diff --git a/gpfsl-examples/stack/proof_treiber_history.v b/gpfsl-examples/stack/proof_treiber_history.v
index a650468b..a473366f 100644
--- a/gpfsl-examples/stack/proof_treiber_history.v
+++ b/gpfsl-examples/stack/proof_treiber_history.v
@@ -1432,7 +1432,7 @@ Lemma StackInv_history_master_acc_instance :
history_master γg 1 E ∗
(history_master γg 1 E -∗ StackInv γg s E).
Proof.
- intros. iDestruct 1 as (?????????) "(? & $ & ?)". unfold StackInv. iIntros "$". eauto 11 with iFrame.
+ intros. iDestruct 1 as (?????????) "(? & $ & ?)". iIntros "$". by iFrame.
Qed.
Lemma StackInv_history_snap_instance :
--
GitLab