From aec517b550114680b9e09975cfae6a32c311c2db Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 2 Dec 2021 17:34:36 -0500
Subject: [PATCH] fix read_contrib_spec_1 being unexpectedly weak for no reason

---
 iris_heap_lang/lib/counter.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index 430fec3d4..8d19bd9e3 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -155,7 +155,7 @@ Section contrib_spec.
 
   Lemma read_contrib_spec_1 γ l n :
     {{{ ccounter_ctx γ l ∗ ccounter γ 1 n }}} read #l
-    {{{ n, RET #n; ccounter γ 1 n }}}.
+    {{{ RET #n; ccounter γ 1 n }}}.
   Proof.
     iIntros (Φ) "[#? Hγf] HΦ".
     rewrite /read /=. wp_lam. iInv N as (c) ">[Hγ Hl]". wp_load.
-- 
GitLab