diff --git a/theories/tests/par_inc.v b/theories/tests/par_inc.v index cf5c208b57b395e41d5d1f8355fe6f3691d3f830..4f8a7baae920522cc61192e2bc6d680c0b1f97bf 100644 --- a/theories/tests/par_inc.v +++ b/theories/tests/par_inc.v @@ -21,7 +21,7 @@ Section par_inc. cl ↦C #n -∗ CWP par_inc (cloc_to_val cl) @ R {{ v, ⌜ v = #2 ⌝ ∧ cl ↦C #(2 + n) }}. Proof. - iIntros "Hl". iApply cwp_fun. + iIntros "Hl". iApply cwp_fun; simpl. iMod (own_alloc (●! 0%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ [Hγ1 Hγ2]]"; [done|]. set (par_inc_inv := (∃ n' : nat, cl ↦C #(n' + n) ∗ own γ (●! n'))%I). iApply (cwp_insert_res _ _ par_inc_inv with "[Hγ Hl]").