Skip to content
Snippets Groups Projects
Commit 3a6eafbb authored by Hai Dang's avatar Hai Dang
Browse files

fix to be compatible with coq 9.0+rc1

parent 0ea042c5
No related branches found
Tags coq-stdpp-1.6.0
1 merge request!44fix to be compatible with Rocq 9.0+rc1
...@@ -55,7 +55,6 @@ Section RelAcqProp. ...@@ -55,7 +55,6 @@ Section RelAcqProp.
Proof. Proof.
unseal. iIntros "obj". unseal. iIntros "obj".
iExists ∅. rewrite -view_at_objectively. iFrame "obj". iExists ∅. rewrite -view_at_objectively. iFrame "obj".
rewrite (_: ( to_latT (∅: threadView) : authR _) = ε) //.
rewrite -embed_bupd. by iApply own_unit. rewrite -embed_bupd. by iApply own_unit.
Qed. Qed.
......
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