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

update dependencies; fix for agree_op rename

parent 176c5169
No related branches found
No related tags found
No related merge requests found
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
"coq-iris" { (= "dev.2020-09-03.1.7dd1b9af") | (= "dev") }
"coq-iris" { (= "dev.2020-09-15.3.986a8883") | (= "dev") }
]
......@@ -113,10 +113,10 @@ Section double.
- iIntros (v1 v2) "[[[H1 Hγ]|H1] [[H2 Hγ']|H2]] !>".
+ by iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
+ iDestruct "H2" as (v2') "(_&H1'&HP)".
iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%agree_op_invL'].
iDestruct (own_valid_2 with "H1 H1'") as %[_ [=->]%to_agree_op_inv_L].
iApply "HΦ"; auto.
+ iDestruct "H1" as (v1') "(_&H2'&HP)".
iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%agree_op_invL'].
iDestruct (own_valid_2 with "H2 H2'") as %[_ [=->]%to_agree_op_inv_L].
iApply "HΦ"; auto.
+ iDestruct "H1" as (v1') "[H1 _]"; iDestruct "H2" as (v2') "(_&H2&_)".
by iDestruct (own_valid_2 with "H1 H2") as %[].
......
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