diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index c886a7693526c938a9754ad0bc141c47a1f53820..7471c3794fa0149955dce239bdaac9c653123f67 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -30,7 +30,7 @@ Section increment.
     wp_apply load_spec.
     (* Prove the atomic shift for load *)
     iDestruct "AUpd" as (F P) "(HF & HP & #AShft)".
-    iExists F, P. iFrame. iIntros "!# * % HP".
+    iExists F, P. iFrame. iIntros "!#" (E ?) "HP".
     iMod ("AShft" with "[%] HP") as (x) "[H↦ Hclose]"; first done.
     iModIntro. iExists (#x, 1%Qp). iFrame. iSplit.
     { iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }