From 40370710b9d07e17f25e2d2bfb242b7fa5add70d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 22 Feb 2018 02:05:26 +0100
Subject: [PATCH] Properly name variable.

---
 theories/heap_lang/lib/increment.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index c886a7693..7471c3794 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". }
-- 
GitLab