From eae111aeea4e9b7e066819f77c3738b983822a12 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Wed, 6 Mar 2024 10:19:22 +0100
Subject: [PATCH] Fix proof after iris/iris!1035.

---
 gpfsl-examples/stack/proof_elim_graph.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/gpfsl-examples/stack/proof_elim_graph.v b/gpfsl-examples/stack/proof_elim_graph.v
index 366cd6dc..5c0c3ec4 100644
--- a/gpfsl-examples/stack/proof_elim_graph.v
+++ b/gpfsl-examples/stack/proof_elim_graph.v
@@ -748,8 +748,8 @@ Lemma StackInv'_graph_master_acc_instance :
   âˆ€ Î³g s q G, StackInv' Î³g s q G âŠ¢
     âˆƒ q', graph_master Î³g q' G âˆ— (graph_master Î³g q' G -âˆ— StackInv' Î³g s q G).
 Proof.
-  intros. iDestruct 1 as (?????????) "[(?&?&?) ?]".
-  iExists _. iFrame. by iIntros "?".
+  intros. iDestruct 1 as (?????????) "[(?&$&?) ?]".
+  iIntros "$". by iFrame.
 Qed.
 
 Lemma StackInv'_graph_snap_instance :
-- 
GitLab