Skip to content
Snippets Groups Projects
Commit aec517b5 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix read_contrib_spec_1 being unexpectedly weak for no reason

parent b230b840
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment