Commit 821b452a authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 0229b2b9
Pipeline #18006 passed with stage
in 16 minutes and 6 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-06-24.3.5ef58527") | (= "dev") }
"coq-iris" { (= "dev.2019-06-26.0.ad3e5066") | (= "dev") }
]
......@@ -50,7 +50,7 @@ Section mset.
iIntros (<- Hvc Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
wp_lam; wp_pures. wp_load. wp_let.
wp_apply (llist_member_spec with "[//]"). iIntros "_".
rewrite (bool_decide_iff _ (v val_for_compare <$> vs)); last set_solver.
rewrite (bool_decide_iff _ (v val_for_compare <$> vs)); last set_solver -Hvc.
rewrite Hvc. iApply "HΦ". iExists l, hd, vs; auto.
Qed.
......@@ -65,7 +65,7 @@ Section mset.
iIntros (<- Hvc ? Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
wp_lam. wp_pures. wp_load. wp_let. wp_apply wp_assert.
wp_apply (llist_member_spec with "[//]"); iIntros "_".
rewrite Hvc bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
rewrite Hvc bool_decide_false /=; last set_solver -Hvc. wp_op; iSplit=> //; iIntros "!>".
wp_seq. wp_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
iApply "HΦ". iExists l, hd', (v :: vs). iFrame "Hl".
rewrite NoDup_cons fmap_cons Hvc. assert (v vs).
......
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