diff --git a/gpfsl-examples/queue/proof_ms_abs_graph.v b/gpfsl-examples/queue/proof_ms_abs_graph.v index 03a716c3ba6c3a58b7b199c0300acfcd67883093..36557462828d90840396c45bd3a05ef899b8c01e 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".