Commit 7a449ae5 authored by Jonas Kastberg's avatar Jonas Kastberg

Merge branch 'master' of https://gitlab.mpi-sws.org/iris/actris

parents d1f06c73 5d799b6f
Pipeline #34159 passed with stage
in 5 minutes and 47 seconds
......@@ -27,10 +27,10 @@ variables:
## Build jobs
build-coq.8.11.2:
build-coq.8.12.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.11.2"
OPAM_PINS: "coq version 8.12.0"
DENY_WARNINGS: "1"
build-iris.dev:
......
......@@ -7,7 +7,7 @@ at POPL'20.
It has been built and tested with the following dependencies
- Coq 8.11.2
- Coq 8.12.0
- The version of Iris in the [opam file](opam)
In order to build, install the above dependencies and then run
......
......@@ -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 %[].
......
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