From 9acb2476e6807399ef41eee08a1bd74cde23c162 Mon Sep 17 00:00:00 2001 From: Dan Frumin <dfrumin@cs.ru.nl> Date: Tue, 10 Oct 2017 13:42:01 +0200 Subject: [PATCH] Remove an unused argument --- theories/heap_lang/lib/counter.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v index 297e55c80..79112c3fa 100644 --- a/theories/heap_lang/lib/counter.v +++ b/theories/heap_lang/lib/counter.v @@ -32,7 +32,7 @@ Section mono_proof. Global Instance mcounter_persistent l n : PersistentP (mcounter l n). Proof. apply _. Qed. - Lemma newcounter_mono_spec (R : iProp Σ) : + Lemma newcounter_mono_spec : {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}. Proof. iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_seq. wp_alloc l as "Hl". -- GitLab