diff --git a/gpfsl/logic/relacq.v b/gpfsl/logic/relacq.v index d7dc2427eeb4e400a007d06fe8ede7b5108bb8af..344530b5b4eea3c27e4a0e16e9795ed7cfbdd989 100644 --- a/gpfsl/logic/relacq.v +++ b/gpfsl/logic/relacq.v @@ -55,7 +55,6 @@ Section RelAcqProp. Proof. unseal. iIntros "obj". iExists ∅. rewrite -view_at_objectively. iFrame "obj". - rewrite (_: (◯ to_latT (∅: threadView) : authR _) = ε) //. rewrite -embed_bupd. by iApply own_unit. Qed.