From a7ca8d5df71fc1cab79a6af97de2f6e3a6ee114b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 May 2023 09:33:29 +0200
Subject: [PATCH] we can use a wand again here

---
 theories/stacked_borrows/logical_state.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/stacked_borrows/logical_state.v b/theories/stacked_borrows/logical_state.v
index 06e4ba70..e622cb81 100644
--- a/theories/stacked_borrows/logical_state.v
+++ b/theories/stacked_borrows/logical_state.v
@@ -807,7 +807,7 @@ Section tainted_tags.
 
   Lemma tag_tainted_interp_alloc σ l n :
     let nt := Tagged σ.(snp) in
-    tag_tainted_interp σ ⊢ tag_tainted_interp (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n nt) σ.(scs) (S σ.(snp)) σ.(snc)).
+    tag_tainted_interp σ -∗ tag_tainted_interp (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n nt) σ.(scs) (S σ.(snp)) σ.(snc)).
   Proof.
     intros nt. iIntros "Htainted".
     iApply (tag_tainted_interp_preserve σ with "Htainted"). { simpl. lia. }
-- 
GitLab