Commit 771f5a3e authored by Robbert Krebbers's avatar Robbert Krebbers

Fix compilation with Coq master.

parent 0b438db2
Pipeline #23454 failed with stage
in 16 minutes and 1 second
......@@ -129,7 +129,8 @@ Section cwp_rules.
iIntros (γ env l I) "#Hflock Hres #Heq".
iMod (flock_res_alloc_cofinite _ (dom (gset lock_res_gname) I) with "Hflock HR1") as (ρ) "[% Hres']"; first done.
pose (I' := <[ρ:=(1%Qp,R1)]>I).
assert (I !! ρ = None) by by eapply not_elem_of_dom.
assert (I !! ρ = None)
by (by eapply (not_elem_of_dom (D:=gset lock_res_gname))).
iSpecialize ("HΦ" $! _ env l I' with "Hflock [Hres Hres'] []").
{ rewrite /flock_resources /I'.
rewrite big_sepM_insert //. iFrame. }
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment