From 654c9f39c01f62373b927f4cbb557e966c13e763 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 8 Oct 2024 16:15:27 +0100
Subject: [PATCH] Layover for
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1082.
---
gpfsl-examples/queue/proof_ms_abs_graph.v | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v
index 03a716c3..36557462 100644
--- a/gpfsl-examples/queue/proof_ms_abs_graph.v
+++ b/gpfsl-examples/queue/proof_ms_abs_graph.v
@@ -1745,7 +1745,10 @@ Proof.
- (* QueueLocal *)
iSplitL "Gs". { by iApply (graph_snap_empty with "Gs"). }
iExists γ, γh, γl. iFrame "I". iExists ηs, s, [], [], [], ∅. simpl.
- iSplit; [done|]. iFrame "LELs LDLs LTs".
+ iSplit; [done|].
+ (* FIXME: [try iFrame] is layover for
+ https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1082 *)
+ iFrame "LELs LDLs"; try iFrame "LTs".
iSplitL "SNh"; last iSplitL "SNt"; last iSplit; last iSplit.
+ iExists th, [Vh]. rewrite shift_0.
rewrite /toHeadHist /toHeadHist' /= insert_empty. iFrame "SNh".
--
GitLab